diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-03 07:05:28 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-03 07:05:28 -0500 |
| commit | 252860a96565f3c73fff7132eb06059c90582bdd (patch) | |
| tree | ca53076f5c619fddd7f1d8f7cbe2e598af316ffa /test/regress/regress0/issue1063-overloading-dt-sel.smt2 | |
| parent | df058b7fb79abaa4e6488449f2307ee29f47efdd (diff) | |
Op overload parser (#1162)
* Update parser for operator overloading.
* Improvements
* Updates
* Add assert
Diffstat (limited to 'test/regress/regress0/issue1063-overloading-dt-sel.smt2')
| -rw-r--r-- | test/regress/regress0/issue1063-overloading-dt-sel.smt2 | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test/regress/regress0/issue1063-overloading-dt-sel.smt2 b/test/regress/regress0/issue1063-overloading-dt-sel.smt2 new file mode 100644 index 000000000..b3316d373 --- /dev/null +++ b/test/regress/regress0/issue1063-overloading-dt-sel.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --lang=smt2.5 +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-datatypes () ((Enum0 (cons (data Int)) (None)))) +(declare-datatypes () ((Enum1 (cons (data Bool)) (None)))) +(declare-fun var_0 () Enum0) +(declare-fun var_1 () Enum1) +(assert (= (data var_0) 5)) +(assert (data var_1)) +(check-sat) |