Warn about infeasible SyGuS conjectures (#6345)

8 files changed, 10 insertions, 6 deletions

diff --git a/test/regress/regress0/sygus/pbe-pred-contra.sy b/test/regress/regress0/sygus/pbe-pred-contra.sy
index 5bd6ebae4..927d1bf0e 100644
--- a/test/regress/regress0/sygus/pbe-pred-contra.sy
+++ b/test/regress/regress0/sygus/pbe-pred-contra.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status -q
 ; EXPECT: unknown
 (set-logic LIA)
 (synth-fun P ((x Int)) Bool)
diff --git a/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy b/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy
index b9bd8e815..abcccd2ab 100644
--- a/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy
+++ b/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unknown
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status -q
 (set-logic SLIA)
 
 (synth-fun f ((col1 String) (col2 String)) String
diff --git a/test/regress/regress1/issue3970-nl-ext-purify.smt2 b/test/regress/regress1/issue3970-nl-ext-purify.smt2
index 5fbddf13d..c19884a63 100644
--- a/test/regress/regress1/issue3970-nl-ext-purify.smt2
+++ b/test/regress/regress1/issue3970-nl-ext-purify.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: unsat
 (set-logic QF_UFNRA)
 (set-option :nl-ext-purify true)
 (set-option :sygus-inference true)
diff --git a/test/regress/regress1/sygus/issue3201.smt2 b/test/regress/regress1/sygus/issue3201.smt2
index 99a555010..f9df0e782 100644
--- a/test/regress/regress1/sygus/issue3201.smt2
+++ b/test/regress/regress1/sygus/issue3201.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inference
+; COMMAND-LINE: --sygus-inference -q
 (set-logic ALL)
 (declare-fun v () Bool)
 (assert false)
diff --git a/test/regress/regress1/sygus/issue3247.smt2 b/test/regress/regress1/sygus/issue3247.smt2
index 6784b8797..a02fbc5ce 100644
--- a/test/regress/regress1/sygus/issue3247.smt2
+++ b/test/regress/regress1/sygus/issue3247.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inference --strings-exp
+; COMMAND-LINE: --sygus-inference --strings-exp -q
 (set-logic ALL)
 (declare-fun a () String) 
 (declare-fun b () String) 
diff --git a/test/regress/regress1/sygus/issue3649.sy b/test/regress/regress1/sygus/issue3649.sy
index b650c4ca6..0f7fc668c 100644
--- a/test/regress/regress1/sygus/issue3649.sy
+++ b/test/regress/regress1/sygus/issue3649.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unknown
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status -q
 (set-logic ALL)
 (synth-fun inv-fn ((i Int) (x (Array Int Int)) (c Int)) Bool)
 
diff --git a/test/regress/regress1/sygus/issue4009-qep.smt2 b/test/regress/regress1/sygus/issue4009-qep.smt2
index cc79954c4..c2cae2ca2 100644
--- a/test/regress/regress1/sygus/issue4009-qep.smt2
+++ b/test/regress/regress1/sygus/issue4009-qep.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inference --sygus-qe-preproc --no-check-unsat-cores
+; COMMAND-LINE: --sygus-inference --sygus-qe-preproc --no-check-unsat-cores -q
 (set-logic ALL)
 (declare-fun a () Real)
 (declare-fun b () Real)
diff --git a/test/regress/regress1/sygus/issue4083-var-shadow.smt2 b/test/regress/regress1/sygus/issue4083-var-shadow.smt2
index bb9434860..91b77bfaa 100644
--- a/test/regress/regress1/sygus/issue4083-var-shadow.smt2
+++ b/test/regress/regress1/sygus/issue4083-var-shadow.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: unsat
 (set-logic ALL)
 (set-option :miniscope-quant true)
 (set-option :sygus-inference true)