Refactor last call for theories, only create one model when quantifiers are enabled. Fix sep.nil preregistration in TheorySep.

2 files changed, 43 insertions, 1 deletions

diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am
index 9d2abaa18..9744cae99 100644
--- a/test/regress/regress0/sep/Makefile.am
+++ b/test/regress/regress0/sep/Makefile.am
@@ -53,7 +53,8 @@ TESTS =	\
   dispose-list-4-init.smt2 \
   wand-0526-sat.smt2 \
   quant_wand.smt2 \
-  fmf-nemp-2.smt2
+  fmf-nemp-2.smt2 \
+  trees-1.smt2
 
 
 FAILING_TESTS =
diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2
new file mode 100644
index 000000000..88e875f70
--- /dev/null
+++ b/test/regress/regress0/sep/trees-1.smt2
@@ -0,0 +1,41 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-sort Loc 0)
+(declare-const loc0 Loc)
+
+(declare-datatypes () ((Node (node (data Int) (left Loc) (right Loc)))))
+
+(declare-const dv Int)
+(declare-const v Loc)
+
+(declare-const dl Int)
+(declare-const l Loc)
+(declare-const dr Int)
+(declare-const r Loc)
+
+(define-fun ten-tree0 ((x Loc) (d Int)) Bool 
+(or (and (emp loc0) (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and (emp loc0) (= l (as sep.nil Loc))) (and (emp loc0) (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10)))))
+
+(declare-const dy Int)
+(declare-const y Loc)
+(declare-const dz Int)
+(declare-const z Loc)
+
+(define-fun ord-tree0 ((x Loc) (d Int)) Bool 
+(or (and (emp loc0) (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and (emp loc0) (= y (as sep.nil Loc))) (and (emp loc0) (= z (as sep.nil Loc)))) (<= dy d) (<= d dz))))
+
+;------- f -------
+(assert (= y (as sep.nil Loc)))
+(assert (= z (as sep.nil Loc)))
+
+(assert (= dy dv))
+(assert (= dz (+ dv 10)))
+;-----------------
+
+(assert (not (= v (as sep.nil Loc))))
+
+(assert (ten-tree0 v dv))
+(assert (not (ord-tree0 v dv)))
+
+(check-sat)