diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-27 22:41:50 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-27 20:41:50 -0700 |
| commit | 3cf5492a8943b71bb4021f1a78cf28cdfafa4289 (patch) | |
| tree | 8beca43fc5c5c085d20afc3c68c8dd829fa1ef57 /src/theory/quantifiers/cegqi | |
| parent | 240c3b41f7f1b907e006a12465037278df05ade1 (diff) | |
Address more coverity warnings (#2394)
Diffstat (limited to 'src/theory/quantifiers/cegqi')
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 2a17f1e36..b90d98ca6 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -517,11 +517,8 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) activateInstantiationVariable(pv, i); //get the instantiator object - Instantiator * vinst = NULL; - std::map< Node, Instantiator * >::iterator itin = d_instantiator.find( pv ); - if( itin!=d_instantiator.end() ){ - vinst = itin->second; - } + Assert(d_instantiator.find(pv) != d_instantiator.end()); + Instantiator* vinst = d_instantiator[pv]; Assert( vinst!=NULL ); d_active_instantiators[pv] = vinst; vinst->reset(this, sf, pv, d_effort); |