diff options
Diffstat (limited to 'test/regress/regress0/decision')
-rw-r--r-- | test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2 | 1 | ||||
-rw-r--r-- | test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect | 3 |
2 files changed, 3 insertions, 1 deletions
diff --git a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2 b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2 index a8f4ff2b9..20230a6fa 100644 --- a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2 +++ b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2 @@ -9,4 +9,5 @@ (declare-fun p () Bool) (assert (and (= a b) (forall ((x U)) (=> (and (= (f x) a) (not (= (f x) b))) p)))) (check-sat) +(get-info :reason-unknown) (exit) diff --git a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect index 9d5c95cdd..e2cc320e1 100644 --- a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect +++ b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect @@ -1,3 +1,4 @@ % COMMAND-LINE: --decision=justification --disable-miniscope-quant-fv --disable-miniscope-quant -% EXPECT: unknown (INCOMPLETE) +% EXPECT: unknown +% EXPECT: (:reason-unknown incomplete) % EXIT: 0 |