summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ceg_instantiator.cpp
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-09-29 17:48:33 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-09-29 17:48:33 -0500
commitb55cdcaee28aebed9f4ea7e4790e0c97249933ae (patch)
tree85a708e846adfe9105d090c510987ae2ff8603d1 /src/theory/quantifiers/ceg_instantiator.cpp
parentbf1597c53ef6b3d5e6ce6b5601d0b3f97fbea9d9 (diff)
Address some coverity warnings, add another stat.
Diffstat (limited to 'src/theory/quantifiers/ceg_instantiator.cpp')
-rw-r--r--src/theory/quantifiers/ceg_instantiator.cpp4
1 files changed, 1 insertions, 3 deletions
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 1f817da88..61a20ad42 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -329,9 +329,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
if( is_cv ){
d_stack_vars.push_back( pv );
}
- if( vinst!=NULL ){
- d_active_instantiators.erase( pv );
- }
+ d_active_instantiators.erase( pv );
unregisterInstantiationVariable( pv );
return false;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback