summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2013-01-28 01:57:20 -0600
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2013-01-28 01:57:20 -0600
commitc5d1a5d8f898bf22c6bbc98f1d484b07706c035b (patch)
tree49b5cc92ea74d720178d60bab2837bf897559813 /src/theory/theory_engine.cpp
parentbcbf52ffbe0416ecf70bdb644017c338c0540793 (diff)
made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced user-level context dependent. this fixes bug 486
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r--src/theory/theory_engine.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a23480eeb..35ed63bed 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -127,7 +127,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
}
// initialize the quantifiers engine
- d_quantEngine = new QuantifiersEngine(context, this);
+ d_quantEngine = new QuantifiersEngine(context, userContext, this);
// build model information if applicable
d_curr_model = new theory::TheoryModel(userContext, "DefaultModel", true);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback