Fail single invocation techniques when utility inference fails. (#3322)

diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp
index 2bb05ad1b79b10d9435c41db8d3e5ff0c07a5bb4..c713ec1ddb3ea5697d635c4d912fb2033621b768 100644 (file)
--- a/src/theory/quantifiers/single_inv_partition.cpp
+++ b/src/theory/quantifiers/single_inv_partition.cpp
@@ -371,6 +371,7 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs,
   else
   {
     Trace("si-prt") << "...failed." << std::endl;
+    return false;
   }
   return true;
 }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index cdf93384e850510f9b44a5a0faa3aea148bb5f3f..d5ce552e6d9ac9c71b5ce7b576217f1ecefaebdd 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1685,6 +1685,7 @@ set(regress_1_tests
   regress1/sygus/issue3201.smt2
   regress1/sygus/issue3205.smt2
   regress1/sygus/issue3247.smt2
+  regress1/sygus/issue3320-quant.sy
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
   regress1/sygus/list-head-x.sy

diff --git a/test/regress/regress1/sygus/issue3320-quant.sy b/test/regress/regress1/sygus/issue3320-quant.sy
new file mode 100644 (file)
index 0000000..a7b7618
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3320-quant.sy
@@ -0,0 +1,9 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic LIA)
+(declare-var x Int)
+(declare-var y Int)
+(synth-fun myfun ((x Int) (y Int)) Bool)
+(constraint (exists ((x Int) (y Int)) (myfun x y)))
+(constraint (exists ((x Int) (y Int)) (not (myfun x y))))
+(check-synth)