Passed

de.uni_freiburg.informatik.ultimate.smtinterpol.model.ModelTest.testLIA

Standard Error

INFO - Confl: 0 Props: 7 Tprops: 0 Decides: 0 RSplits: 0
INFO - Times: Expl: 0.0 Prop: 0.008 PropClause: 0.113 Set: 0.048 Check: 0.007 Back: 0.0
INFO - Atoms: 7/7 Clauses: 0 Axioms: 19
INFO - CCTimes: iE 0 eq 0 cc 0 setRep 0
INFO - Merges: 0, cc:0
INFO - Hooray, we found a model:
INFO - Equivalence Classes:
INFO - true
INFO - false
INFO - Confl: 0 Props: 6 Tprops: 0 Decides: 0 RSplits: 0
INFO - Times: Expl: 0.0 Prop: 1.465 PropClause: 0.035 Set: 0.161 Check: 1.789 Back: 0.0
INFO - Atoms: 6/6 Cla
...[truncated 5397 chars]...

INFO - Time for pivoting         : 0
INFO - Time for bound computation: 0
INFO - Time for bound setting    : 0
INFO - Time for bound comp(back) : 0
INFO - Composite::createLit: 0
INFO - Number of cuts: 0
INFO - Time for cut-generation: 0
INFO - Count/Time for getUpperBound: 0 / 0.000
INFO - Number of branchings: 0
INFO - Hooray, we found a model:
INFO - Equivalence Classes:
INFO - true
INFO - false
INFO - (f x)=0
INFO - (+ x 5)
INFO - (f (+ x 5))=x
INFO - Assignments:
INFO - x = 5
INFO - y = 1