Fix to ignore a case of triggers with no free variables.

4 files changed, 97 insertions, 5 deletions

diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index c91194239..214a4d055 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -284,7 +284,7 @@ bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) {
         return true;
       }
     }
-  }else if( isAtomicTrigger( n1 ) && isUsable( n1, q ) ){
+  }else if( isUsableAtomicTrigger( n1, q ) ){
     if( options::relationalTriggers() && n2.getKind()==INST_CONSTANT && !quantifiers::TermDb::containsTerm( n1, n2 ) ){
       return true;
     }else if( !quantifiers::TermDb::hasInstConstAttr(n2) ){
@@ -339,15 +339,18 @@ Node Trigger::getIsUsableTrigger( Node n, Node q ) {
       return rtr2;
     }
   }else{
-    bool usable = quantifiers::TermDb::getInstConstAttr(n)==q && isAtomicTrigger( n ) && isUsable( n, q );
-    Trace("trigger-debug") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==q) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl;
-    if( usable ){
+    Trace("trigger-debug") << n << " usable : " << ( quantifiers::TermDb::getInstConstAttr(n)==q ) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl;
+    if( isUsableAtomicTrigger( n, q ) ){
       return pol ? n : NodeManager::currentNM()->mkNode( IFF, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
     }
   }
   return Node::null();
 }
 
+bool Trigger::isUsableAtomicTrigger( Node n, Node q ) {
+  return quantifiers::TermDb::getInstConstAttr( n )==q && isAtomicTrigger( n ) && isUsable( n, q );
+}
+
 bool Trigger::isUsableTrigger( Node n, Node q ){
   Node nu = getIsUsableTrigger( n, q );
   return !nu.isNull();
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 902f73e75..a3da4d398 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -107,6 +107,7 @@ class Trigger {
   /** is usable trigger */
   static bool isUsableTrigger( Node n, Node q );
   static Node getIsUsableTrigger( Node n, Node q );
+  static bool isUsableAtomicTrigger( Node n, Node q );
   static bool isAtomicTrigger( Node n );
   static bool isAtomicTriggerKind( Kind k );
   static bool isRelationalTrigger( Node n );
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index f6d65958e..4c657adf1 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -82,7 +82,8 @@ TESTS =	\
 	parametric-lists.smt2 \
 	partial-trigger.smt2 \
 	inst-max-level-segf.smt2 \
-	small-bug1-fixpoint-3.smt2
+	small-bug1-fixpoint-3.smt2 \
+	z3.620661-no-fv-trigger.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/z3.620661-no-fv-trigger.smt2 b/test/regress/regress0/quantifiers/z3.620661-no-fv-trigger.smt2
new file mode 100644
index 000000000..aad2a4691
--- /dev/null
+++ b/test/regress/regress0/quantifiers/z3.620661-no-fv-trigger.smt2
@@ -0,0 +1,87 @@
+(set-logic AUFNIRA)
+(set-info :status unsat)
+(declare-sort S1 0)
+(declare-sort S2 0)
+(declare-sort S3 0)
+(declare-sort S4 0)
+(declare-sort S5 0)
+(declare-sort S6 0)
+(declare-sort S7 0)
+(declare-sort S8 0)
+(declare-sort S9 0)
+(declare-sort S10 0)
+(declare-sort S11 0)
+(declare-sort S12 0)
+(declare-sort S13 0)
+(declare-fun f1 () S1)
+(declare-fun f2 () S1)
+(declare-fun f3 (S2 Real) Real)
+(declare-fun f4 (S3 Real) S2)
+(declare-fun f5 () S3)
+(declare-fun f6 (S4 Int) Int)
+(declare-fun f7 (S5 Int) S4)
+(declare-fun f8 () S5)
+(declare-fun f9 () S2)
+(declare-fun f10 () Real)
+(declare-fun f11 () Real)
+(declare-fun f12 () S2)
+(declare-fun f13 (S7 S6) Real)
+(declare-fun f14 () S7)
+(declare-fun f15 () S2)
+(declare-fun f16 () S2)
+(declare-fun f17 (S8 Int) S6)
+(declare-fun f18 () S8)
+(declare-fun f19 (S9 S6) Int)
+(declare-fun f20 () S9)
+(declare-fun f21 (S10 Real) S7)
+(declare-fun f22 () S10)
+(declare-fun f23 () S2)
+(declare-fun f24 (S11 S6) S6)
+(declare-fun f25 (S12 S6) S11)
+(declare-fun f26 () S12)
+(declare-fun f27 () S12)
+(declare-fun f28 (S13 Int) S9)
+(declare-fun f29 () S13)
+(declare-fun f30 () S2)
+(declare-fun f31 () S4)
+(assert (not (= f1 f2)))
+(assert (forall ((?v0 Real) (?v1 Real)) (= (f3 (f4 f5 ?v0) ?v1) (* ?v0 ?v1))))
+(assert (forall ((?v0 Int) (?v1 Int)) (= (f6 (f7 f8 ?v0) ?v1) (* ?v0 ?v1))))
+(assert (not (= (f3 f9 (- f10 f11)) (- (f3 f9 f10)))))
+(assert (= (f3 f9 f11) 0.0))
+(assert (forall ((?v0 Real)) (= (f3 f9 (+ f11 ?v0)) (- (f3 f9 ?v0)))))
+(assert (= (f3 f9 (/ f11 2.0)) 1.0))
+(assert (= (f3 f9 (/ f11 6.0)) (/ 1.0 2.0)))
+(assert (= (f3 f9 (* 2.0 f11)) 0.0))
+(assert (= (f3 f9 (* (/ 3.0 2.0) f11)) (- 1.0)))
+(assert (let ((?v_0 2.0)) (<= (/ f11 ?v_0) ?v_0)))
+(assert (let ((?v_0 2.0)) (< (/ f11 ?v_0) ?v_0)))
+(assert (< (- (* 2.0 f11)) f11))
+(assert (< (- (/ f11 2.0)) 0.0))
+(assert (<= 2.0 f11))
+(assert (<= 0.0 (/ f11 2.0)))
+(assert (< 0.0 (/ f11 2.0)))
+(assert (< f11 4.0))
+(assert (<= 0.0 f11))
+(assert (< 0.0 f11))
+(assert (let ((?v_0 2.0)) (not (= (/ f11 ?v_0) ?v_0))))
+(assert (not (= (/ f11 2.0) 0.0)))
+(assert (not (< f11 0.0)))
+(assert (not (= f11 0.0)))
+(assert (forall ((?v0 S6) (?v1 S6)) (= (= (f13 f14 ?v0) (f13 f14 ?v1)) (= ?v0 ?v1))))
+(assert (forall ((?v0 S6) (?v1 S6)) (= (< (f13 f14 ?v0) (f13 f14 ?v1)) (< (f19 f20 ?v0) (f19 f20 ?v1)))))
+(assert (forall ((?v0 S6) (?v1 S6)) (= (<= (f13 f14 ?v0) (f13 f14 ?v1)) (<= (f19 f20 ?v0) (f19 f20 ?v1)))))
+(assert (forall ((?v0 S6) (?v1 S6)) (let ((?v_0 (f19 f20 ?v1)) (?v_1 (f19 f20 ?v0))) (=> (<= ?v_1 ?v_0) (= (f13 f14 (f17 f18 (- ?v_0 ?v_1))) (- (f13 f14 ?v1) (f13 f14 ?v0)))))))
+(assert (forall ((?v0 Real) (?v1 Real)) (exists ((?v2 Real) (?v3 Real)) (and (= ?v0 (* ?v2 (f3 f15 ?v3))) (= ?v1 (* ?v2 (f3 f9 ?v3)))))))
+(assert (< 1.0 (f3 f16 2.0)))
+(assert (< 0.0 (f3 f16 2.0)))
+(assert (<= 0.0 (f3 f16 2.0)))
+(assert (forall ((?v0 Real) (?v1 Real)) (<= 0.0 (f3 f16 (+ (* ?v0 ?v0) (* ?v1 ?v1))))))
+(assert (forall ((?v0 Real) (?v1 Real)) (=> (<= ?v0 ?v1) (<= (f3 f16 ?v0) (f3 f16 ?v1)))))
+(assert (forall ((?v0 Real) (?v1 Real)) (=> (< ?v0 ?v1) (< (f3 f16 ?v0) (f3 f16 ?v1)))))
+(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (<= ?v_0 ?v0) (=> (= (f3 f16 ?v0) ?v_0) (= ?v0 ?v_0))))))
+(assert (forall ((?v0 Real)) (=> (< 0.0 ?v0) (< (/ ?v0 (f3 f16 2.0)) ?v0))))
+(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (<= ?v_0 ?v0) (<= ?v_0 (f3 f16 ?v0))))))
+(assert (forall ((?v0 Real)) (let ((?v_0 1.0)) (=> (<= ?v_0 ?v0) (<= ?v_0 (f3 f16 ?v0))))))
+(check-sat)
+(exit)