Fix E-matching for case where candidate generator is not properly initialized (#2708)

3 files changed, 48 insertions, 0 deletions

diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 78fb987f1..646208ec6 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -384,6 +384,11 @@ void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){
 }
 
 bool InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
+  if (d_cg == nullptr)
+  {
+    // we did not properly initialize the candidate generator, thus we fail
+    return false;
+  }
   eqc = qe->getEqualityQuery()->getRepresentative( eqc );
   Trace("matching-debug2") << this << " reset " << eqc << "." << std::endl;
   if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()!=INST_CONSTANT ){
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c4dbab1dd..a8eced69e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1359,6 +1359,7 @@ set(regress_1_tests
   regress1/quantifiers/quant-wf-int-ind.smt2
   regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2
   regress1/quantifiers/recfact.cvc
+  regress1/quantifiers/rel-trigger-unusable.smt2
   regress1/quantifiers/repair-const-nterm.smt2
   regress1/quantifiers/rew-to-0211-dd.smt2
   regress1/quantifiers/ricart-agrawala6.smt2
diff --git a/test/regress/regress1/quantifiers/rel-trigger-unusable.smt2 b/test/regress/regress1/quantifiers/rel-trigger-unusable.smt2
new file mode 100644
index 000000000..f3bf1f693
--- /dev/null
+++ b/test/regress/regress1/quantifiers/rel-trigger-unusable.smt2
@@ -0,0 +1,42 @@
+; COMMAND-LINE: --relational-triggers --full-saturate-quant
+; EXPECT: unsat
+(set-logic UFNIA)
+(set-info :status unsat)
+
+(declare-fun two_to_the (Int) Int)
+
+
+;other definitions
+(define-fun intmax ((k Int)) Int (- (two_to_the k) 1))
+(define-fun intmodtotal ((k Int) (a Int) (b Int)) Int (ite (= b 0) a (mod a b)))
+(define-fun intnot ((k Int) (a Int)) Int (- (intmax k) a))
+(define-fun intadd ((k Int) (a Int) (b Int) ) Int (intmodtotal k (+ a b) (two_to_the k)))
+
+;l and SC
+(define-fun l ((k Int) (x Int) (s Int) (t Int)) Bool  (distinct (intadd k x s) t))
+(define-fun SC ((k Int) (s Int) (t Int)) Bool true)
+
+;conditional inverse
+(define-fun inv ((k Int) (s Int) (t Int)) Int (intnot k (intadd k s t)))
+
+(declare-fun k () Int)
+(declare-fun s () Int)
+(declare-fun t () Int)
+
+(define-fun left_to_right ((k Int) (s Int) (t Int)) Bool (=> (SC k s t) (l k (inv k s t) s t)))
+(define-fun assertion_ltr () Bool (not (left_to_right k s t)))
+
+;range helpers (everything between 0 and 2^k)
+(define-fun in_range ((k Int) (x Int)) Bool (and (>= x 0) (< x (two_to_the k))))
+(define-fun range_assumptions ((k Int) (s Int) (t Int)) Bool (and (>= k 1) (in_range k s) (in_range k t)))
+
+;original assertions
+(assert (range_assumptions k s t))
+
+(assert assertion_ltr)
+(declare-fun dummy (Int) Bool)
+(assert (dummy t))
+(assert (forall ((x Int)) (! (=> (>= x 0) (and (dummy x) (distinct (- (two_to_the k) 1) (* 2 x)))) :pattern ((dummy x))) ))
+
+; relational-triggers segfaulted this previous due to a quantified formula that only has a relational trigger, which is unusable
+(check-sat)