summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.cpp
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-06-01 15:51:39 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-06-01 15:51:47 -0500
commit6edc4fac0e5c868b6c6bad13ffc9112b16c1d5f5 (patch)
tree2d89d797c3b2cf856be60234013c7dae9efae258 /src/theory/quantifiers_engine.cpp
parentae5236eeda43ff591b9264d653727d4ae7d1de68 (diff)
Initial infrastructure for bounded set quantification (disabled). Refactoring and fixes for --fmf-bound-int. Fix simple memory leaks in strings and bounded integers.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r--src/theory/quantifiers_engine.cpp1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8b51e94b5..2bebabc5a 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -634,6 +634,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
//check whether we should apply a reduction
if( reduceQuantifier( f ) ){
+ Trace("quant") << "...reduced." << std::endl;
d_quants[f] = false;
return false;
}else{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback