projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c5f6528) | patch
After blasting the disjuncts, TheoryEngine rewrite needs to reinvoke itself. QF_LRA...
authorTim King <taking@cs.nyu.edu>
Sat, 29 May 2010 00:14:09 +0000 (00:14 +0000)
committerTim King <taking@cs.nyu.edu>
Sat, 29 May 2010 00:14:09 +0000 (00:14 +0000)
commit49c2b740513ad4e6a256e1758575bd898afbdfc5
tree2f857f4d546499e2b488477a38cb35e38930e270tree
parentc5f652834b915641ae6cbeccf97e959470757863commit | diff
After blasting the disjuncts, TheoryEngine rewrite needs to reinvoke itself. QF_LRA is now no longer complaining about seeing nodes that can be rewritten to CONST_BOOLEAN.
src/theory/theory_engine.cpp diff | blob | history