summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sep/wand-simp-sat2.smt2
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-07-07 17:14:56 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-07-07 17:14:56 -0500
commit730e277a542602f36fc548e8face6b8209b2bb94 (patch)
treeff6f14eb55d7420c99ab7e1b925019c098445114 /test/regress/regress0/sep/wand-simp-sat2.smt2
parentf62609d9eca8086d5c68b77cfd0a5d717d24aeab (diff)
Ensure heap disjointness in sep refinements.
Diffstat (limited to 'test/regress/regress0/sep/wand-simp-sat2.smt2')
-rwxr-xr-xtest/regress/regress0/sep/wand-simp-sat2.smt23
1 files changed, 2 insertions, 1 deletions
diff --git a/test/regress/regress0/sep/wand-simp-sat2.smt2 b/test/regress/regress0/sep/wand-simp-sat2.smt2
index ebc115fdd..059e91317 100755
--- a/test/regress/regress0/sep/wand-simp-sat2.smt2
+++ b/test/regress/regress0/sep/wand-simp-sat2.smt2
@@ -1,6 +1,7 @@
; COMMAND-LINE: --no-check-models
-; EXPECT: unsat
+; EXPECT: sat
(set-logic ALL_SUPPORTED)
+(set-info :status sat)
(declare-fun x () Int)
(assert (wand (pto x 1) (pto x 3)))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback