summaryrefslogtreecommitdiff
path: root/test/regress/regress0/issue1063-overloading-dt-sel.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/issue1063-overloading-dt-sel.smt2')
-rw-r--r--test/regress/regress0/issue1063-overloading-dt-sel.smt25
1 files changed, 2 insertions, 3 deletions
diff --git a/test/regress/regress0/issue1063-overloading-dt-sel.smt2 b/test/regress/regress0/issue1063-overloading-dt-sel.smt2
index b3316d373..390c9acad 100644
--- a/test/regress/regress0/issue1063-overloading-dt-sel.smt2
+++ b/test/regress/regress0/issue1063-overloading-dt-sel.smt2
@@ -1,9 +1,8 @@
-; 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-datatypes ((Enum0 0)) (((cons (data Int)) (None))))
+(declare-datatypes ((Enum1 0)) (((cons (data Bool)) (None))))
(declare-fun var_0 () Enum0)
(declare-fun var_1 () Enum1)
(assert (= (data var_0) 5))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback