diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-22 11:01:05 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-22 11:01:05 +0200 |
| commit | a7a9ba359a2a8a26f20ac8fdf5292c4e0e27c76a (patch) | |
| tree | a62e3c29bb702a2e890b234504bbc121c4da2619 /test/regress/regress0/bug519.smt2 | |
| parent | 7e133dbb7c1adf077102d377d1f7eecae1640ee1 (diff) | |
Enable counterexample-guided quantifier instantiation by default for quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions.
Diffstat (limited to 'test/regress/regress0/bug519.smt2')
| -rw-r--r-- | test/regress/regress0/bug519.smt2 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/regress0/bug519.smt2 b/test/regress/regress0/bug519.smt2 index 406cb0c1b..72ec634a8 100644 --- a/test/regress/regress0/bug519.smt2 +++ b/test/regress/regress0/bug519.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: -mi --tlimit-per 1000 -; EXPECT: unknown +; COMMAND-LINE: -mi +; EXPECT: sat ; EXPECT: unsat (set-logic ALL_SUPPORTED) |