Support for separation logic + EPR. Refactor preprocessing of sep.nil, only allow sep disequal card constants when type is monotonic. Update logics on sep regressions.

37 files changed, 49 insertions, 36 deletions

diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am
index 6078bfa19..7bcd700bd 100644
--- a/test/regress/regress0/sep/Makefile.am
+++ b/test/regress/regress0/sep/Makefile.am
@@ -56,7 +56,8 @@ TESTS =	\
   fmf-nemp-2.smt2 \
   trees-1.smt2 \
   wand-false.smt2 \
-  dup-nemp.smt2
+  dup-nemp.smt2 \
+  emp2-quant-unsat.smt2
 
 
 FAILING_TESTS =
diff --git a/test/regress/regress0/sep/chain-int.smt2 b/test/regress/regress0/sep/chain-int.smt2
index d3245e33f..ebe52fa46 100644
--- a/test/regress/regress0/sep/chain-int.smt2
+++ b/test/regress/regress0/sep/chain-int.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/crash1220.smt2 b/test/regress/regress0/sep/crash1220.smt2
index a0fc5a187..f68434f33 100755
--- a/test/regress/regress0/sep/crash1220.smt2
+++ b/test/regress/regress0/sep/crash1220.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/dispose-list-4-init.smt2 b/test/regress/regress0/sep/dispose-list-4-init.smt2
index 766354cd9..b3e2088b1 100644
--- a/test/regress/regress0/sep/dispose-list-4-init.smt2
+++ b/test/regress/regress0/sep/dispose-list-4-init.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 
 (declare-sort Loc 0)
 
diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2
index 009561128..98348f617 100644
--- a/test/regress/regress0/sep/dup-nemp.smt2
+++ b/test/regress/regress0/sep/dup-nemp.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 (declare-sort Loc 0)
 (declare-const l Loc)
diff --git a/test/regress/regress0/sep/emp2-quant-unsat.smt2 b/test/regress/regress0/sep/emp2-quant-unsat.smt2
new file mode 100644
index 000000000..52d99d8c0
--- /dev/null
+++ b/test/regress/regress0/sep/emp2-quant-unsat.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --quant-epr
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-sort U 0)
+(declare-fun u () U)
+
+(assert (sep (not (emp u)) (not (emp u))))
+
+(assert (forall ((x U) (y U)) (= x y)))
+
+(check-sat)
diff --git a/test/regress/regress0/sep/loop-1220.smt2 b/test/regress/regress0/sep/loop-1220.smt2
index 2981606d8..b857aec2a 100644
--- a/test/regress/regress0/sep/loop-1220.smt2
+++ b/test/regress/regress0/sep/loop-1220.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2
index e1e21dd10..a0766a7e0 100644
--- a/test/regress/regress0/sep/nemp.smt2
+++ b/test/regress/regress0/sep/nemp.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (assert (not (emp 0)))
 (check-sat)
diff --git a/test/regress/regress0/sep/nspatial-simp.smt2 b/test/regress/regress0/sep/nspatial-simp.smt2
index 0c93719c9..c807757d1 100755
--- a/test/regress/regress0/sep/nspatial-simp.smt2
+++ b/test/regress/regress0/sep/nspatial-simp.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 (declare-fun x () Int)
 
diff --git a/test/regress/regress0/sep/pto-01.smt2 b/test/regress/regress0/sep/pto-01.smt2
index b0dece248..28ed5c47b 100644
--- a/test/regress/regress0/sep/pto-01.smt2
+++ b/test/regress/regress0/sep/pto-01.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/pto-02.smt2 b/test/regress/regress0/sep/pto-02.smt2
index f0b6d2dee..ab1cea0c8 100644
--- a/test/regress/regress0/sep/pto-02.smt2
+++ b/test/regress/regress0/sep/pto-02.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 
diff --git a/test/regress/regress0/sep/pto-04.smt2 b/test/regress/regress0/sep/pto-04.smt2
index 1734c93bb..9b0afda7a 100644
--- a/test/regress/regress0/sep/pto-04.smt2
+++ b/test/regress/regress0/sep/pto-04.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x1 Int)
diff --git a/test/regress/regress0/sep/sep-01.smt2 b/test/regress/regress0/sep/sep-01.smt2
index c3330f036..a93fc4db8 100644
--- a/test/regress/regress0/sep/sep-01.smt2
+++ b/test/regress/regress0/sep/sep-01.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-02.smt2 b/test/regress/regress0/sep/sep-02.smt2
index 403bcf077..6f190d964 100644
--- a/test/regress/regress0/sep/sep-02.smt2
+++ b/test/regress/regress0/sep/sep-02.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-03.smt2 b/test/regress/regress0/sep/sep-03.smt2
index 427c44b50..8dce5acc7 100644
--- a/test/regress/regress0/sep/sep-03.smt2
+++ b/test/regress/regress0/sep/sep-03.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-find2.smt2 b/test/regress/regress0/sep/sep-find2.smt2
index 26a27eb22..356f866c1 100644
--- a/test/regress/regress0/sep/sep-find2.smt2
+++ b/test/regress/regress0/sep/sep-find2.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x1 Int)
diff --git a/test/regress/regress0/sep/sep-neg-1refine.smt2 b/test/regress/regress0/sep/sep-neg-1refine.smt2
index 8ddbdd05f..ab12c6461 100644
--- a/test/regress/regress0/sep/sep-neg-1refine.smt2
+++ b/test/regress/regress0/sep/sep-neg-1refine.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-neg-nstrict.smt2 b/test/regress/regress0/sep/sep-neg-nstrict.smt2
index 1a69336a8..425e5ce3c 100644
--- a/test/regress/regress0/sep/sep-neg-nstrict.smt2
+++ b/test/regress/regress0/sep/sep-neg-nstrict.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-neg-nstrict2.smt2 b/test/regress/regress0/sep/sep-neg-nstrict2.smt2
index e71e6a51a..7ada6ff06 100644
--- a/test/regress/regress0/sep/sep-neg-nstrict2.smt2
+++ b/test/regress/regress0/sep/sep-neg-nstrict2.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-neg-simple.smt2 b/test/regress/regress0/sep/sep-neg-simple.smt2
index 191e7527f..7b6fc69e9 100644
--- a/test/regress/regress0/sep/sep-neg-simple.smt2
+++ b/test/regress/regress0/sep/sep-neg-simple.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-neg-swap.smt2 b/test/regress/regress0/sep/sep-neg-swap.smt2
index f89a9c0ac..53f890b0d 100644
--- a/test/regress/regress0/sep/sep-neg-swap.smt2
+++ b/test/regress/regress0/sep/sep-neg-swap.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-nterm-again.smt2 b/test/regress/regress0/sep/sep-nterm-again.smt2
index 9b4afe36a..3e595b5e9 100644
--- a/test/regress/regress0/sep/sep-nterm-again.smt2
+++ b/test/regress/regress0/sep/sep-nterm-again.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-nterm-val-model.smt2 b/test/regress/regress0/sep/sep-nterm-val-model.smt2
index 0178134cb..d4fb0fd52 100644
--- a/test/regress/regress0/sep/sep-nterm-val-model.smt2
+++ b/test/regress/regress0/sep/sep-nterm-val-model.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-plus1.smt2 b/test/regress/regress0/sep/sep-plus1.smt2
index 772acd981..9522e2420 100644
--- a/test/regress/regress0/sep/sep-plus1.smt2
+++ b/test/regress/regress0/sep/sep-plus1.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/sep-simp-unc.smt2 b/test/regress/regress0/sep/sep-simp-unc.smt2
index 6cdf51294..cedbb53eb 100755
--- a/test/regress/regress0/sep/sep-simp-unc.smt2
+++ b/test/regress/regress0/sep/sep-simp-unc.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 (declare-sort U 0)
 (declare-fun x () U)
diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
index fb58b9d10..9239fb770 100644
--- a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
+++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-sort U 0)
diff --git a/test/regress/regress0/sep/simple-neg-sat.smt2 b/test/regress/regress0/sep/simple-neg-sat.smt2
index 0c0b6a9a3..70927ad82 100644
--- a/test/regress/regress0/sep/simple-neg-sat.smt2
+++ b/test/regress/regress0/sep/simple-neg-sat.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2
index ed3187a96..10e509e05 100644
--- a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2
+++ b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/split-find-unsat.smt2 b/test/regress/regress0/sep/split-find-unsat.smt2
index 1731174fa..1a9e76a8a 100644
--- a/test/regress/regress0/sep/split-find-unsat.smt2
+++ b/test/regress/regress0/sep/split-find-unsat.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-const x Int)
diff --git a/test/regress/regress0/sep/wand-0526-sat.smt2 b/test/regress/regress0/sep/wand-0526-sat.smt2
index 0c0ee72ad..fa0aab591 100644
--- a/test/regress/regress0/sep/wand-0526-sat.smt2
+++ b/test/regress/regress0/sep/wand-0526-sat.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (declare-fun x () Int)
 (declare-fun y () Int)
 (declare-fun u () Int)
diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2
index 9b4871323..1d799c8c9 100644
--- a/test/regress/regress0/sep/wand-crash.smt2
+++ b/test/regress/regress0/sep/wand-crash.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (assert (wand (emp 0) (emp 0)))
 (check-sat)
diff --git a/test/regress/regress0/sep/wand-false.smt2 b/test/regress/regress0/sep/wand-false.smt2
index 642c0a8aa..65500f775 100644
--- a/test/regress/regress0/sep/wand-false.smt2
+++ b/test/regress/regress0/sep/wand-false.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 (declare-fun x () Int)
 (assert (wand (pto x x) false))
diff --git a/test/regress/regress0/sep/wand-nterm-simp.smt2 b/test/regress/regress0/sep/wand-nterm-simp.smt2
index e8ee4252c..0db7330d1 100644
--- a/test/regress/regress0/sep/wand-nterm-simp.smt2
+++ b/test/regress/regress0/sep/wand-nterm-simp.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (declare-fun x () Int)
 (assert (wand (emp x) (pto x 3)))
 (check-sat)
diff --git a/test/regress/regress0/sep/wand-nterm-simp2.smt2 b/test/regress/regress0/sep/wand-nterm-simp2.smt2
index c317e8736..cce0f79e3 100644
--- a/test/regress/regress0/sep/wand-nterm-simp2.smt2
+++ b/test/regress/regress0/sep/wand-nterm-simp2.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 (declare-fun x () Int)
 (assert (wand (pto x 1) (emp x)))
diff --git a/test/regress/regress0/sep/wand-simp-sat.smt2 b/test/regress/regress0/sep/wand-simp-sat.smt2
index df4bfa6d8..120683f74 100755
--- a/test/regress/regress0/sep/wand-simp-sat.smt2
+++ b/test/regress/regress0/sep/wand-simp-sat.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (declare-fun x () Int)
 (assert (wand (pto x 1) (pto x 1)))
 (check-sat)
diff --git a/test/regress/regress0/sep/wand-simp-sat2.smt2 b/test/regress/regress0/sep/wand-simp-sat2.smt2
index 059e91317..c684d16ad 100755
--- a/test/regress/regress0/sep/wand-simp-sat2.smt2
+++ b/test/regress/regress0/sep/wand-simp-sat2.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: sat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)
 (declare-fun x () Int)
 (assert (wand (pto x 1) (pto x 3)))
diff --git a/test/regress/regress0/sep/wand-simp-unsat.smt2 b/test/regress/regress0/sep/wand-simp-unsat.smt2
index 95bc85537..c9851661a 100755
--- a/test/regress/regress0/sep/wand-simp-unsat.smt2
+++ b/test/regress/regress0/sep/wand-simp-unsat.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models
 ; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (declare-fun x () Int)
 (assert (wand (pto x 1) (pto x 3)))
 (assert (emp x))