diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-11 16:29:21 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-11 16:29:21 -0500 |
| commit | 3e6de62d11dcb3cf266f58e68def2f2c2ce728c3 (patch) | |
| tree | dfccefc822de0cdfe5165b429b2bb356740eddc6 /test/regress | |
| parent | 09be883cb1e27635426a3ca6c296a3557a07f2e0 (diff) | |
Fix constructor type printing (#3246)
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/dt-param-2.6-print.smt2 | 20 |
2 files changed, 21 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5b44128fc..56010858d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -360,6 +360,7 @@ set(regress_0_tests regress0/datatypes/dt-2.6.smt2 regress0/datatypes/dt-match-pat-param-2.6.smt2 regress0/datatypes/dt-param-2.6.smt2 + regress0/datatypes/dt-param-2.6-print.smt2 regress0/datatypes/dt-param-card4-bool-sat.smt2 regress0/datatypes/dt-sel-2.6.smt2 regress0/datatypes/empty_tuprec.cvc diff --git a/test/regress/regress0/datatypes/dt-param-2.6-print.smt2 b/test/regress/regress0/datatypes/dt-param-2.6-print.smt2 new file mode 100644 index 000000000..165de0dba --- /dev/null +++ b/test/regress/regress0/datatypes/dt-param-2.6-print.smt2 @@ -0,0 +1,20 @@ +; EXPECT: sat +; EXPECT: (model +; EXPECT: (declare-datatypes ((Pair 2)) ((par (X Y)((mkPair (first X) (second Y)))))) +; EXPECT: (define-fun x () (Pair Int Real) ((as mkPair (Pair Int Real)) 2 (/ 3 2))) +; EXPECT: ) + +(set-logic ALL) +(set-option :produce-models true) +(set-info :status sat) +(declare-datatypes ( (Pair 2) ) ( +(par ( X Y ) ( (mkPair (first X) (second Y)))) +)) + + +(declare-fun x () (Pair Int Real)) + +(assert (= x (mkPair 2 1.5))) + +(check-sat) +(get-model) |