Fix issue with multi-triggers that include variable triggers (#1810)

3 files changed, 37 insertions, 28 deletions

diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 9c3095e59..3ceefcd90 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -142,21 +142,22 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
       for (unsigned i = 0, size = d_match_pattern.getNumChildren(); i < size;
            i++)
       {
-        Node qa = quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i]);
+        Node pat = d_match_pattern[i];
+        Node qa = quantifiers::TermUtil::getInstConstAttr(pat);
         if (!qa.isNull())
         {
-          InstMatchGenerator* cimg =
-              getInstMatchGenerator(q, d_match_pattern[i]);
-          if (cimg)
+          if (pat.getKind() == INST_CONSTANT && qa == q)
           {
-            d_children.push_back(cimg);
-            d_children_index.push_back(i);
-            d_children_types.push_back(-2);
-          }else{
-            if (d_match_pattern[i].getKind() == INST_CONSTANT && qa == q)
+            d_children_types.push_back(pat.getAttribute(InstVarNumAttribute()));
+          }
+          else
+          {
+            InstMatchGenerator* cimg = getInstMatchGenerator(q, pat);
+            if (cimg)
             {
-              d_children_types.push_back(
-                  d_match_pattern[i].getAttribute(InstVarNumAttribute()));
+              d_children.push_back(cimg);
+              d_children_index.push_back(i);
+              d_children_types.push_back(-2);
             }
             else
             {
@@ -535,24 +536,23 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, std::vecto
 
 InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n)
 {
-  if (n.getKind() == INST_CONSTANT)
+  if (n.getKind() != INST_CONSTANT)
   {
-    return NULL;
-  }
-  Trace("var-trigger-debug") << "Is " << n << " a variable trigger?"
-                             << std::endl;
-  Node x;
-  if (options::purifyTriggers())
-  {
-    x = Trigger::getInversionVariable(n);
-  }
-  if (!x.isNull())
-  {
-    Node s = Trigger::getInversion(n, x);
-    VarMatchGeneratorTermSubs* vmg = new VarMatchGeneratorTermSubs(x, s);
-    Trace("var-trigger") << "Term substitution trigger : " << n
-                         << ", var = " << x << ", subs = " << s << std::endl;
-    return vmg;
+    Trace("var-trigger-debug")
+        << "Is " << n << " a variable trigger?" << std::endl;
+    Node x;
+    if (options::purifyTriggers())
+    {
+      x = Trigger::getInversionVariable(n);
+    }
+    if (!x.isNull())
+    {
+      Node s = Trigger::getInversion(n, x);
+      VarMatchGeneratorTermSubs* vmg = new VarMatchGeneratorTermSubs(x, s);
+      Trace("var-trigger") << "Term substitution trigger : " << n
+                           << ", var = " << x << ", subs = " << s << std::endl;
+      return vmg;
+    }
   }
   return new InstMatchGenerator(n);
 }
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 88ea4ebd5..e8149316c 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -593,6 +593,7 @@ REG0_TESTS = \
 	regress0/quantifiers/ex3.smt2 \
 	regress0/quantifiers/ex6.smt2 \
 	regress0/quantifiers/floor.smt2 \
+	regress0/quantifiers/issue1805.smt2 \
 	regress0/quantifiers/is-even-pred.smt2 \
 	regress0/quantifiers/is-int.smt2 \
 	regress0/quantifiers/lra-triv-gn.smt2 \
diff --git a/test/regress/regress0/quantifiers/issue1805.smt2 b/test/regress/regress0/quantifiers/issue1805.smt2
new file mode 100644
index 000000000..929522dec
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue1805.smt2
@@ -0,0 +1,8 @@
+(set-logic AUFBVDTNIRA)
+(set-info :status unsat)
+(declare-fun abs1 (Int) Int)
+(assert
+  (forall ((x Int) (y Int))
+  (! (= (<= (abs1 x) y) (and (<= (- y) x) (<= x y))) :pattern ((abs1 x) y) )))
+(assert (< (abs1 (- 3)) 3))
+(check-sat)