projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 66033cd) | patch
bug fixes in justification heuristic
authorKshitij Bansal <kshitij@cs.nyu.edu>
Thu, 14 Jun 2012 21:08:28 +0000 (21:08 +0000)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Thu, 14 Jun 2012 21:08:28 +0000 (21:08 +0000)
commitc43514fef548f977e88e2986c2f993b975830cc2
tree4362eb7aab0de2376813a07cbc6cc37d781528b0tree
parent66033cd2059d817cdeab5adc25f1397532a3fa78commit | diff
bug fixes in justification heuristic
* remove assert iteSkolemMap gives ite-s (not true with repeatSimp)
* handle a corner case in findSplitter triggered by repeatSimp
src/decision/justification_heuristic.cpp diff | blob | history
test/regress/regress0/decision/Makefile.am diff | blob | history
test/regress/regress0/decision/error122.delta01.smt [new file with mode: 0644] blob
test/regress/regress0/decision/error122.smt [new file with mode: 0644] blob
test/regress/regress0/decision/error20.delta01.smt [new file with mode: 0644] blob
test/regress/regress0/decision/error20.smt [new file with mode: 0644] blob