diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-08-26 18:56:39 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-08-26 19:22:08 -0400 |
| commit | 8f9362dcd60e31bbb9300c0f20662afb3dc0c185 (patch) | |
| tree | 7328e8b7e67a06f9db8bfb07cc9483ac04b8b9e3 /test/regress/regress0 | |
| parent | 48418b76615dde8d5b472f773358ea1e05890767 (diff) | |
bug 374 fix: assert litVal=desiredVal only for leaf nodes1.1.x
Conflicts:
src/decision/justification_heuristic.cpp
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/decision/Makefile.am | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am index 4bba7b049..42fedd480 100644 --- a/test/regress/regress0/decision/Makefile.am +++ b/test/regress/regress0/decision/Makefile.am @@ -27,6 +27,8 @@ TESTS = \ uflia-xs-09-16-3-4-1-5.delta03.smt \ aufbv-fuzz01.smt \ bug347.smt \ + bug374a.smt \ + bug374b.smt2 \ error20.smt \ error20.delta01.smt \ error122.smt \ @@ -54,6 +56,8 @@ EXTRA_DIST = $(TESTS) \ quant-Arrays_Q1-noinfer.smt2.expect \ wchains010ue.delta02.smt.expect \ bug347.smt.expect \ + bug374a.smt.expect \ + bug374b.smt2.expect \ quant-ex1.disable_miniscope.smt2.expect \ wchains010ue.smt.expect \ just_sat.expect \ |