summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sygus
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/sygus')
-rw-r--r--test/regress/regress1/sygus/constant-bool-si-all.sy2
-rw-r--r--test/regress/regress1/sygus/constant-dec-tree-bug.sy2
-rw-r--r--test/regress/regress1/sygus/sygus-uf-ex.sy4
-rw-r--r--test/regress/regress1/sygus/tester.sy2
4 files changed, 5 insertions, 5 deletions
diff --git a/test/regress/regress1/sygus/constant-bool-si-all.sy b/test/regress/regress1/sygus/constant-bool-si-all.sy
index eee7956f4..45d49e75b 100644
--- a/test/regress/regress1/sygus/constant-bool-si-all.sy
+++ b/test/regress/regress1/sygus/constant-bool-si-all.sy
@@ -1,6 +1,6 @@
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
-(set-logic SAT)
+(set-logic LIA)
(synth-fun f () Bool)
(synth-fun g () Bool)
(synth-fun h () Bool)
diff --git a/test/regress/regress1/sygus/constant-dec-tree-bug.sy b/test/regress/regress1/sygus/constant-dec-tree-bug.sy
index 7229dea2e..e20520a4a 100644
--- a/test/regress/regress1/sygus/constant-dec-tree-bug.sy
+++ b/test/regress/regress1/sygus/constant-dec-tree-bug.sy
@@ -1,7 +1,7 @@
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status --sygus-unif-pi=complete
-(set-logic SAT)
+(set-logic LIA)
(synth-fun u ((x Int)) Int)
(synth-fun f () Bool)
(synth-fun g () Bool)
diff --git a/test/regress/regress1/sygus/sygus-uf-ex.sy b/test/regress/regress1/sygus/sygus-uf-ex.sy
index b9731de0f..66880eafa 100644
--- a/test/regress/regress1/sygus/sygus-uf-ex.sy
+++ b/test/regress/regress1/sygus/sygus-uf-ex.sy
@@ -1,6 +1,6 @@
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
-(set-logic LIA)
+; COMMAND-LINE: --sygus-out=status --uf-ho
+(set-logic UFLIA)
(declare-fun uf ( Int ) Int)
(synth-fun f ((x Int) (y Int)) Bool
((Start Bool (true false
diff --git a/test/regress/regress1/sygus/tester.sy b/test/regress/regress1/sygus/tester.sy
index bf1cd1576..282bc122c 100644
--- a/test/regress/regress1/sygus/tester.sy
+++ b/test/regress/regress1/sygus/tester.sy
@@ -1,7 +1,7 @@
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
-(set-logic SLIA)
+(set-logic DTSLIA)
(declare-datatype DT ((A (a Int)) (B (b String)) (JSBool (jsBool Bool))))
(define-fun isA ((i DT)) Bool ((_ is A) i) )
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback