diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2013-10-24 16:48:30 -0700 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2013-10-24 16:48:30 -0700 |
| commit | 0274d973ae504fa74fd73aa80c725a778581bb26 (patch) | |
| tree | a1cbd99f2e75721a9467c77c8cbbe2c7ce7a8c87 /src/theory/model.h | |
| parent | 496c5489a5073ef1aa9306e165ac4dc4aaeb69a9 (diff) | |
Fix for bug515
Diffstat (limited to 'src/theory/model.h')
| -rw-r--r-- | src/theory/model.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/model.h b/src/theory/model.h index 03a641df4..a18d66ab0 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -42,8 +42,11 @@ protected: public: TheoryModel(context::Context* c, std::string name, bool enableFuncModels); virtual ~TheoryModel(){} + + /** special local context for our equalityEngine so we can clear it independently of search context */ + context::Context* d_eeContext; /** equality engine containing all known equalities/disequalities */ - eq::EqualityEngine d_equalityEngine; + eq::EqualityEngine* d_equalityEngine; /** map of representatives of equality engine to used representatives in representative set */ std::map< Node, Node > d_reps; /** stores set of representatives for each type */ |