diff options
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/jsat-2.6.smt2 | 28 |
2 files changed, 30 insertions, 1 deletions
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index caf1fc61c..b437f1878 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -80,7 +80,8 @@ TESTS = \ dt-param-2.6.smt2 \ dt-color-2.6.smt2 \ dt-match-pat-param-2.6.smt2 \ - tuple-no-clash.cvc + tuple-no-clash.cvc \ + jsat-2.6.smt2 FAILING_TESTS = \ datatype-dump.cvc diff --git a/test/regress/regress0/datatypes/jsat-2.6.smt2 b/test/regress/regress0/datatypes/jsat-2.6.smt2 new file mode 100644 index 000000000..7e7fe4f49 --- /dev/null +++ b/test/regress/regress0/datatypes/jsat-2.6.smt2 @@ -0,0 +1,28 @@ +; COMMAND-LINE: --lang=smt2.6 +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero)) +((cons (car tree) (cdr list)) (null)) +((node (children list)) (leaf (data nat))) +)) +(declare-fun x1 () nat) +(declare-fun x2 () nat) +(declare-fun x3 () nat) +(declare-fun x4 () nat) +(declare-fun x5 () nat) +(declare-fun x6 () list) +(declare-fun x7 () list) +(declare-fun x8 () list) +(declare-fun x9 () list) +(declare-fun x10 () list) +(declare-fun x11 () tree) +(declare-fun x12 () tree) +(declare-fun x13 () tree) +(declare-fun x14 () tree) +(declare-fun x15 () tree) + +(assert (and (and (= x9 x7) ((_ is node) x11)) (not ((_ is zero) x5)))) +(check-sat) + + |