summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.h
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-03-16 13:57:53 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-03-16 13:57:53 -0500
commiteb27070783709a410e6655ba9af6da6de5b0da9d (patch)
treec4fcb9203e2e72c9a96a51641ac15207f292a75b /src/theory/quantifiers_engine.h
parentfd3844131f334e929bfb04eb2dcb6229cf1190cd (diff)
Change internal representative selection for finite domains that do not involve uninterpreted sorts, including bounded integer quantification.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r--src/theory/quantifiers_engine.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 0c43223d8..228ac9ee9 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -203,7 +203,7 @@ private:
std::map< Node, int > d_total_inst_debug;
std::map< Node, int > d_temp_inst_debug;
int d_total_inst_count_debug;
- /** inst round counters */
+ /** inst round counters TODO: make context-dependent? */
int d_ierCounter;
int d_ierCounter_lc;
int d_ierCounterLastLc;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback