From 1a2547995acc5a98c8969e628ac5e1c45b0efe94 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 17 Jun 2016 15:55:56 -0500 Subject: Support for separation logic. Enable cbqi by default for pure BV. --- test/regress/regress0/sep/sep-simp-unc.smt2 | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100755 test/regress/regress0/sep/sep-simp-unc.smt2 (limited to 'test/regress/regress0/sep/sep-simp-unc.smt2') diff --git a/test/regress/regress0/sep/sep-simp-unc.smt2 b/test/regress/regress0/sep/sep-simp-unc.smt2 new file mode 100755 index 000000000..6cdf51294 --- /dev/null +++ b/test/regress/regress0/sep/sep-simp-unc.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-sort U 0) +(declare-fun x () U) +(declare-fun y () U) +(declare-fun a () U) +(declare-fun b () U) + +(assert (not (sep (not (pto x a)) (pto y b)))) +(check-sat) -- cgit v1.2.3