1 files changed, 12 insertions, 12 deletions

diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index 9c8560783..bbae46df7 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -104,7 +104,7 @@ void testAnd() {
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::AND, a, b, c) );
+      d_nodeManager->mkNode(kind::AND, a, b, c), false);
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -125,13 +125,13 @@ void testComplexExpr() {
               d_nodeManager->mkNode(kind::OR, c, d),
               d_nodeManager->mkNode(
                   kind::NOT,
-                  d_nodeManager->mkNode(kind::XOR, e, f)))) );
+                  d_nodeManager->mkNode(kind::XOR, e, f)))), false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
 void testFalse() {
   NodeManagerScope nms(d_nodeManager);
-  d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false) );
+  d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -140,7 +140,7 @@ void testIff() {
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::IFF, a, b) );
+      d_nodeManager->mkNode(kind::IFF, a, b), false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -149,7 +149,7 @@ void testImplies() {
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::IMPLIES, a, b) );
+      d_nodeManager->mkNode(kind::IMPLIES, a, b), false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -165,7 +165,7 @@ void testIte() {
               d_nodeManager->mkVar(d_nodeManager->integerType())
           ),
           d_nodeManager->mkVar(d_nodeManager->integerType())
-                            ));
+                            ), false);
 
 }
 
@@ -173,7 +173,7 @@ void testNot() {
   NodeManagerScope nms(d_nodeManager);
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::NOT, a) );
+      d_nodeManager->mkNode(kind::NOT, a), false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -183,13 +183,13 @@ void testOr() {
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::OR, a, b, c) );
+      d_nodeManager->mkNode(kind::OR, a, b, c), false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
 void testTrue() {
   NodeManagerScope nms(d_nodeManager);
-  d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true) );
+  d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -197,10 +197,10 @@ void testVar() {
   NodeManagerScope nms(d_nodeManager);
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-  d_cnfStream->convertAndAssert(a);
+  d_cnfStream->convertAndAssert(a, false);
   TS_ASSERT( d_satSolver->addClauseCalled() );
   d_satSolver->reset();
-  d_cnfStream->convertAndAssert(b);
+  d_cnfStream->convertAndAssert(b, false);
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -209,7 +209,7 @@ void testXor() {
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::XOR, a, b) );
+      d_nodeManager->mkNode(kind::XOR, a, b), false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 };