1 files changed, 41 insertions, 0 deletions
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)