From dd29958ff0c78c099f540f080e455d843caf1c6b Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 23 Jan 2020 15:53:48 -0600
Subject: [PATCH] Fix trivial solve method for single invocation (#3650)

---
 .../sygus/ce_guided_single_inv.cpp            |  2 +-
 test/regress/CMakeLists.txt                   |  1 +
 test/regress/regress1/sygus/issue3654.sy      | 24 +++++++++++++++++++
 3 files changed, 26 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress1/sygus/issue3654.sy

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index e36047e67..b6750c5da 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -676,7 +676,7 @@ bool CegSingleInv::solveTrivial(Node q)
     }
   }
   // if we solved all arguments
-  if (args.empty())
+  if (args.empty() && body.isConst() && !body.getConst<bool>())
   {
     Trace("cegqi-si-trivial-solve")
         << q << " is trivially solvable by substitution " << vars << " -> "
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 65d7f2b31..518e3a889 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1787,6 +1787,7 @@ set(regress_1_tests
   regress1/sygus/issue3580.sy
   regress1/sygus/issue3634.smt2
   regress1/sygus/issue3635.smt2
+  regress1/sygus/issue3654.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/issue3654.sy b/test/regress/regress1/sygus/issue3654.sy
new file mode 100644
index 000000000..12949c55a
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3654.sy
@@ -0,0 +1,24 @@
+; EXPECT: unknown
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+(synth-fun inv-fn ((i Int) (x (Array Int Int)) (c Int)) Bool)
+
+(define-fun init-fn ((i Int) (x (Array Int Int)) (c Int)) Bool 
+	(and (= i 0)
+	(= (select x 10) c)))
+
+(define-fun post-fn ((i Int) (x (Array Int Int))(c Int)) Bool 
+	(exists ((index Int)) (and (= (select x index) c)
+	(forall ((index2 Int)) (=> (< index2 index) (not (= (select x index) c))))
+	)))
+
+(declare-var x (Array Int Int))
+(declare-var x! (Array Int Int))
+(declare-var i Int)
+(declare-var i! Int)
+(declare-var c Int)
+
+	
+(constraint (=> (init-fn i x c) (inv-fn i x c)))
+(constraint (=> (inv-fn i x c) (post-fn i x c)))
+(check-synth)
-- 
2.30.2