Passed

de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CongruentAddTest.testCase3

Standard Error

DEBUG - Created Equality: true == false
DEBUG - Added Ground Clause: [!(true == false)]
DEBUG - Created Equality: a == b
DEBUG - Created Equality: b == c
DEBUG - Created Equality: c == d
DEBUG - createAppTerm (f c) congruent: null
DEBUG - createAppTerm (f b) congruent: null
DEBUG - createAppTerm (f x0) congruent: null
DEBUG - M x0 x1
DEBUG - createAppTerm (f x1) congruent: (f x0)
DEBUG - addPendingCongruence: (f x1) (f x0)
DEBUG - PC ((f x1),(f x0))
DEBUG - M (f x1) (f x0)
DEBUG - Created Equali
...[truncated 2808 chars]...
 congruent: (f c)
DEBUG - addPendingCongruence: (f d) (f c)
INFO - f(d)-creation time: 45364 ns
DEBUG - PC ((f d),(f c))
DEBUG - M (f c) (f d)
DEBUG - B b == c
DEBUG - U (f c) (f d)
DEBUG - U (f b) (f a)
DEBUG - U (f c) (f b)
DEBUG - U b c
DEBUG - Still congruent: (f a) and (f b)
DEBUG - addPendingCongruence: (f a) (f b)
DEBUG - Still congruent: (f d) and (f c)
DEBUG - addPendingCongruence: (f d) (f c)
DEBUG - PC ((f a),(f b))
DEBUG - M (f a) (f b)
DEBUG - PC ((f d),(f c))
DEBUG - M (f d) (f c)