fix sharing issue for portfolio (full lit-to-node map wasn't being kept in my previous checkin)

3 files changed, 7 insertions, 5 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 7f1456639..681e42a99 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -55,8 +55,8 @@ void CnfStream::recordTranslation(TNode node) {
   }
 }
 
-TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar) :
-  CnfStream(satSolver, registrar) {
+TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar, bool fullLitToNodeMap) :
+  CnfStream(satSolver, registrar, fullLitToNodeMap) {
 }
 
 void CnfStream::assertClause(TNode node, SatClause& c) {
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index c9fd4a08b..4b16a02b9 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -187,7 +187,7 @@ public:
    * @param satSolver the sat solver to use
    * @param registrar the entity that takes care of preregistration of Nodes
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
-   * even for non-theory literals.
+   * even for non-theory literals
    */
   CnfStream(SatInputInterface* satSolver, theory::Registrar registrar, bool fullLitToNodeMap = false);
 
@@ -286,8 +286,10 @@ public:
    * Constructs the stream to use the given sat solver.
    * @param satSolver the sat solver to use
    * @param registrar the entity that takes care of pre-registration of Nodes
+   * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
+   * even for non-theory literals
    */
-  TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar);
+  TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar, bool fullLitToNodeMap = false);
 
 private:
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 9b0b93f78..3430fd7c6 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -73,7 +73,7 @@ PropEngine::PropEngine(TheoryEngine* te, Context* context) :
   d_satSolver = new SatSolver(this, d_theoryEngine, d_context);
 
   theory::Registrar registrar(d_theoryEngine);
-  d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar);
+  d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar, Options::current()->threads > 1);
 
   d_satSolver->setCnfStream(d_cnfStream);
 }