diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/repeated-selectors-2769.smt2 | 10 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/tree-get-value.cvc | 10 | ||||
| -rw-r--r-- | test/regress/regress0/printer/tuples_and_records.cvc | 18 |
4 files changed, 41 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c8b052265..6f147db3c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -371,11 +371,13 @@ set(regress_0_tests regress0/datatypes/rec1.cvc regress0/datatypes/rec2.cvc regress0/datatypes/rec4.cvc + regress0/datatypes/repeated-selectors-2769.smt2 regress0/datatypes/rewriter.cvc regress0/datatypes/sc-cdt1.smt2 regress0/datatypes/some-boolean-tests.cvc regress0/datatypes/stream-singleton.smt2 regress0/datatypes/tenum-bug.smt2 + regress0/datatypes/tree-get-value.cvc regress0/datatypes/tuple-model.cvc regress0/datatypes/tuple-no-clash.cvc regress0/datatypes/tuple-record-bug.cvc @@ -572,6 +574,7 @@ set(regress_0_tests regress0/print_lambda.cvc regress0/printer/bv_consts_bin.smt2 regress0/printer/bv_consts_dec.smt2 + regress0/printer/tuples_and_records.cvc regress0/push-pop/boolean/fuzz_12.smt2 regress0/push-pop/boolean/fuzz_13.smt2 regress0/push-pop/boolean/fuzz_14.smt2 diff --git a/test/regress/regress0/datatypes/repeated-selectors-2769.smt2 b/test/regress/regress0/datatypes/repeated-selectors-2769.smt2 new file mode 100644 index 000000000..827b17e36 --- /dev/null +++ b/test/regress/regress0/datatypes/repeated-selectors-2769.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL) +(set-info :status sat) +(declare-datatypes ((t1 1)) ((par (T1) ((mkt1 (p1 T1)))))) +(declare-datatypes ((t2 1)) ((par (T1) ((mkt2 (p1 T1)))))) +(define-fun s1 () (t1 Int) (mkt1 3)) +(define-fun s2 () (t2 Int) (mkt2 3)) +(define-fun s3 () Int (p1 s1)) +(define-fun s4 () Int (p1 s2)) +(assert (= s3 s4)) +(check-sat) diff --git a/test/regress/regress0/datatypes/tree-get-value.cvc b/test/regress/regress0/datatypes/tree-get-value.cvc new file mode 100644 index 000000000..0a7da7f69 --- /dev/null +++ b/test/regress/regress0/datatypes/tree-get-value.cvc @@ -0,0 +1,10 @@ +% EXPECT: sat +% EXPECT: ((left(x), leaf)) +OPTION "produce-models"; +DATATYPE + tree = node(left : tree, right : tree) | leaf +END; +x : tree; +ASSERT is_leaf(left(x)); +CHECKSAT; +GET_VALUE left(x); diff --git a/test/regress/regress0/printer/tuples_and_records.cvc b/test/regress/regress0/printer/tuples_and_records.cvc new file mode 100644 index 000000000..267a316e8 --- /dev/null +++ b/test/regress/regress0/printer/tuples_and_records.cvc @@ -0,0 +1,18 @@ +% EXPECT: invalid +% EXPECT: ((r.a, "active")) +% EXPECT: ((y.1, 9)) +OPTION "produce-models"; + +R : TYPE = [# + a : STRING, + b : STRING +#]; +r : R; + +y: [REAL, INT, REAL]; + +ASSERT r = (# a := "active", b := "who knows?" #); +ASSERT y = ( 4/5, 9, 11/9 ); +QUERY r.a = "what?"; +GET_VALUE r.a; +GET_VALUE y.1; |