diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-21 09:42:07 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-21 09:42:07 +0100 |
| commit | 32b0aba2c2c27ad038d34c8554a4bae76e8dd363 (patch) | |
| tree | e6e737d10b53c0c13dfba072cdec6d1f9b5449a2 /test | |
| parent | f70804a7159390fcb01d8c1ec208fbfd8e544fba (diff) | |
Change default option to --inst-when=full-last-call (interleave instantiation and theory combination). Fix inefficiency in NNF, enable by default. Set best defaults for --mbqi=abs.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/quantifiers/burns4.smt2 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test/regress/regress0/quantifiers/burns4.smt2 b/test/regress/regress0/quantifiers/burns4.smt2 index 886d6f5c8..72023fd4f 100644 --- a/test/regress/regress0/quantifiers/burns4.smt2 +++ b/test/regress/regress0/quantifiers/burns4.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat (set-logic AUFLIA) (set-info :source | Burns mutual exclusion protocol. This is a benchmark of the haRVey theorem prover. It was translated to SMT-LIB by Leonardo de Moura |) (set-info :smt-lib-version 2.0) |