diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/sep/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/sep/trees-1.smt2 | 41 |
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) |