diff options
Diffstat (limited to 'test/regress/regress1/sygus')
| -rw-r--r-- | test/regress/regress1/sygus/clock-inc-tuple.sy | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/error1-dt.sy | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/extract.sy | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/issue3461.sy | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/list-head-x.sy | 2 |
5 files changed, 5 insertions, 5 deletions
diff --git a/test/regress/regress1/sygus/clock-inc-tuple.sy b/test/regress/regress1/sygus/clock-inc-tuple.sy index b5d7bff91..5af4407f7 100644 --- a/test/regress/regress1/sygus/clock-inc-tuple.sy +++ b/test/regress/regress1/sygus/clock-inc-tuple.sy @@ -1,7 +1,7 @@ ; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-var m Int) (declare-var s Int) (declare-var inc Int) diff --git a/test/regress/regress1/sygus/error1-dt.sy b/test/regress/regress1/sygus/error1-dt.sy index d0027d685..9b57339db 100644 --- a/test/regress/regress1/sygus/error1-dt.sy +++ b/test/regress/regress1/sygus/error1-dt.sy @@ -1,7 +1,7 @@ ; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none --sygus-active-gen=enum -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatypes ((IntRange 0)) (((IntRange (lower Int) (upper Int))))) diff --git a/test/regress/regress1/sygus/extract.sy b/test/regress/regress1/sygus/extract.sy index f3cfa09a2..fef48f364 100644 --- a/test/regress/regress1/sygus/extract.sy +++ b/test/regress/regress1/sygus/extract.sy @@ -1,7 +1,7 @@ ; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatype Ex ((Ex2 (ex Int))))
(synth-fun ident ((x1 Ex)) Int
diff --git a/test/regress/regress1/sygus/issue3461.sy b/test/regress/regress1/sygus/issue3461.sy index 08b5738c1..ebd6dd346 100644 --- a/test/regress/regress1/sygus/issue3461.sy +++ b/test/regress/regress1/sygus/issue3461.sy @@ -1,7 +1,7 @@ ; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --sygus-out=status -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatype Doc ((D (owner Int) (body Int)))) diff --git a/test/regress/regress1/sygus/list-head-x.sy b/test/regress/regress1/sygus/list-head-x.sy index c6b7d032a..f1c99a28f 100644 --- a/test/regress/regress1/sygus/list-head-x.sy +++ b/test/regress/regress1/sygus/list-head-x.sy @@ -1,6 +1,6 @@ ; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil)))) |