diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-09 16:14:31 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-09 16:14:42 -0600 |
| commit | 19697d530ae6eaf0165270bc3628f76124a45953 (patch) | |
| tree | baa129ef51cc45295dc9f2f7cc176ca27768f4f9 /test/regress/regress0/decision | |
| parent | b3f5d2860747c2608c0d765d105c8dd32ee57e1d (diff) | |
More complete guess instantiation strategy, cvc4 now typically times out instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc
Diffstat (limited to 'test/regress/regress0/decision')
| -rw-r--r-- | test/regress/regress0/decision/Makefile.am | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am index 366204191..90a18f0e2 100644 --- a/test/regress/regress0/decision/Makefile.am +++ b/test/regress/regress0/decision/Makefile.am @@ -25,7 +25,6 @@ TESTS = \ bitvec5.smt \ quant-Arrays_Q1-noinfer.smt2 \ quant-ex1.smt2 \ - quant-ex1.disable_miniscope.smt2 \ uflia-xs-09-16-3-4-1-5.delta03.smt \ aufbv-fuzz01.smt \ bug347.smt \ |