Passed

de.uni_freiburg.informatik.ultimate.smtinterpol.dpll.AllSatTest.testAllSat

Standard Error

DEBUG - Created Equality: true == false
DEBUG - Added Ground Clause: [!(true == false)]
TRACE - Added clause [!(true == false)]
DEBUG - Creating var x
DEBUG - Creating var y
DEBUG - Generated LinVar x + y
DEBUG - Added Ground Clause: [[-468187696]x + y >= 0]
TRACE - Added clause [[-468187696]x + y >= 0]
DEBUG - DPLL: propagate theories
DEBUG - S !(true == false)
DEBUG - DPLL: propagate theories
DEBUG - S [-468187696]x + y >= 0
DEBUG - DPLL: propagate theories
DEBUG - DPLL: checkpoint
DEBUG - DPL
...[truncated 4779 chars]...
INFO - Number of branchings: 0
INFO - Hooray, we found a model:
INFO - Equivalence Classes:
INFO - true
INFO - false
DEBUG - Shared Vars:
INFO - Assignments:
INFO - x = 1
INFO - y = -1
TRACE - -2040938575: !(true == false)
TRACE - 468187695: [-468187696]x + y >= 0
TRACE - 729021703: [729021703]y <= -1
TRACE - 122773685: [-122773686]x >= 0
Found minterm:
(not (< x 0))
(< y 0)
(not (= (* 2 x) 1))
(= x x)
DEBUG - explain conflict [[-122773686]x <= -1, [729021703]y >= 0]
DEBUG - removing level0: []