diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/theory/theory_arith_white.cpp | 2 | ||||
-rw-r--r-- | test/unit/theory/theory_bv_white.cpp | 6 | ||||
-rw-r--r-- | test/unit/theory/theory_quantifiers_bv_inverter_white.cpp | 4 |
3 files changed, 6 insertions, 6 deletions
diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp index 5e5b52d3e..4c8834c8d 100644 --- a/test/unit/theory/theory_arith_white.cpp +++ b/test/unit/theory/theory_arith_white.cpp @@ -41,7 +41,7 @@ class TestTheoryWhiteArith : public TestSmtNoFinishInit void SetUp() override { TestSmtNoFinishInit::SetUp(); - d_smtEngine->setOption("incremental", CVC4::SExpr(false)); + d_smtEngine->setOption("incremental", "false"); d_smtEngine->finishInit(); d_context = d_smtEngine->getContext(); d_user_context = d_smtEngine->getUserContext(); diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp index c07f2c402..976724c8e 100644 --- a/test/unit/theory/theory_bv_white.cpp +++ b/test/unit/theory/theory_bv_white.cpp @@ -43,8 +43,8 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core) { d_smtEngine->setLogic("QF_BV"); - d_smtEngine->setOption("bitblast", SExpr("eager")); - d_smtEngine->setOption("incremental", SExpr("false")); + d_smtEngine->setOption("bitblast", "eager"); + d_smtEngine->setOption("incremental", "false"); // Notice that this unit test uses the theory engine of a created SMT // engine d_smtEngine. We must ensure that d_smtEngine is properly initialized // via the following call, which constructs its underlying theory engine. @@ -72,7 +72,7 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core) TEST_F(TestTheoryWhiteBv, mkUmulo) { - d_smtEngine->setOption("incremental", SExpr("true")); + d_smtEngine->setOption("incremental", "true"); for (uint32_t w = 1; w < 16; ++w) { d_smtEngine->push(); diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp index 5c222d2c1..b5996a684 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp @@ -35,8 +35,8 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit void SetUp() override { TestSmtNoFinishInit::SetUp(); - d_smtEngine->setOption("cegqi-full", CVC4::SExpr(true)); - d_smtEngine->setOption("produce-models", CVC4::SExpr(true)); + d_smtEngine->setOption("cegqi-full", "true"); + d_smtEngine->setOption("produce-models", "true"); d_smtEngine->finishInit(); d_s = d_nodeManager->mkVar("s", d_nodeManager->mkBitVectorType(4)); |