diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-19 17:29:44 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-11-19 17:29:44 -0600 |
| commit | d7f5a6f2fa4b82b729e8ea76ef580c2bdb804e4e (patch) | |
| tree | 39f8c9b8fca6b5c6d4dd74fd46b5820e41e159c5 /src/theory/quantifiers/ematching | |
| parent | c163ebf20b2728515479e1f43d2beaa4ecf46944 (diff) | |
Fix E-matching for case where candidate generator is not properly initialized (#2708)
Diffstat (limited to 'src/theory/quantifiers/ematching')
| -rw-r--r-- | src/theory/quantifiers/ematching/inst_match_generator.cpp | 5 |
1 files changed, 5 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 ){ |