incorporate a fix from smtcomp2010 version for handling CNF of (= bool bool); also...
authorMorgan Deters <mdeters@gmail.com>
Thu, 22 Jul 2010 21:55:28 +0000 (21:55 +0000)
committerMorgan Deters <mdeters@gmail.com>
Thu, 22 Jul 2010 21:55:28 +0000 (21:55 +0000)
commit62ec86743289b26241d69b1701d4b3f547ee2bed
treefc4d460a9326eaae1e481cf0f48ff6c15738150e
parent27a24d7f553a0b3981e18418a67edb3c4bfa52e9
incorporate a fix from smtcomp2010 version for handling CNF of (= bool bool); also make theoryOf(= t1 t2) return theoryOf(t1.getType()), rather than theoryOf(t1), as the latter gives different results for (= (geq x1 x2) (leq x2 x1)) and (= a (leq x2 x1)), which is strange and causes problems.  should discuss at tuesday meeting.  resolves bug 187.
src/prop/cnf_stream.cpp
src/theory/theory_engine.cpp
src/theory/theory_engine.h
test/unit/theory/theory_engine_white.h