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/quantifiers | |
| 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/quantifiers')
| -rw-r--r-- | test/regress/regress0/quantifiers/bug291.smt2 | 1 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/bug291.smt2.expect | 3 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 | 2 |
3 files changed, 2 insertions, 4 deletions
diff --git a/test/regress/regress0/quantifiers/bug291.smt2 b/test/regress/regress0/quantifiers/bug291.smt2 index b39e415a8..dbc230599 100644 --- a/test/regress/regress0/quantifiers/bug291.smt2 +++ b/test/regress/regress0/quantifiers/bug291.smt2 @@ -10,5 +10,4 @@ (declare-fun store2 (Int) Int) (assert (forall ((?A Int) (?o Int) (?f Int) (?p Int) (?g Int) (?v Int)) (=> (not (= ?o ?p)) (= (select2 (store2 ?A)) (select2 ?A))))) (check-sat) -(get-info :reason-unknown) (exit) diff --git a/test/regress/regress0/quantifiers/bug291.smt2.expect b/test/regress/regress0/quantifiers/bug291.smt2.expect index 2bd8349de..7856f23b4 100644 --- a/test/regress/regress0/quantifiers/bug291.smt2.expect +++ b/test/regress/regress0/quantifiers/bug291.smt2.expect @@ -1,2 +1 @@ -% EXPECT: unknown -% EXPECT: (:reason-unknown incomplete) +% EXPECT: sat diff --git a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 index e8d53669c..bd7ca19cd 100644 --- a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 +++ b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi2 +; COMMAND-LINE: --dt-rewrite-error-sel ; EXPECT: unsat (set-logic ALL_SUPPORTED) (declare-datatypes () ((List (cons (head Int) (tail List)) (nil)))) |