diff options
Diffstat (limited to 'src/theory/ee_manager_distributed.cpp')
-rw-r--r-- | src/theory/ee_manager_distributed.cpp | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp index 360b1257b..3fb5fc0ce 100644 --- a/src/theory/ee_manager_distributed.cpp +++ b/src/theory/ee_manager_distributed.cpp @@ -34,6 +34,18 @@ EqEngineManagerDistributed::~EqEngineManagerDistributed() void EqEngineManagerDistributed::initializeTheories() { context::Context* c = d_te.getSatContext(); + // initialize the shared solver + EeSetupInfo esis; + if (d_sharedSolver.needsEqualityEngine(esis)) + { + // allocate an equality engine for the shared terms database + d_stbEqualityEngine.reset(allocateEqualityEngine(esis, c)); + d_sharedSolver.setEqualityEngine(d_stbEqualityEngine.get()); + } + else + { + Unhandled() << "Expected shared solver to use equality engine"; + } // allocate equality engines per theory for (TheoryId theoryId = theory::THEORY_FIRST; |