diff options
Diffstat (limited to 'test/unit/theory/theory_bv_opt_white.cpp')
| -rw-r--r-- | test/unit/theory/theory_bv_opt_white.cpp | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp index c23ce79dd..5cd29878e 100644 --- a/test/unit/theory/theory_bv_opt_white.cpp +++ b/test/unit/theory/theory_bv_opt_white.cpp @@ -57,9 +57,9 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min) d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(), BitVector(32u, (uint32_t)0x3FFFFFA1)); @@ -78,9 +78,9 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min) d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, true); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); BitVector val = d_optslv->getValues()[0].getValue().getConst<BitVector>(); std::cout << "opt value is: " << val << std::endl; @@ -105,9 +105,9 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max) d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, false); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); BitVector val = d_optslv->getValues()[0].getValue().getConst<BitVector>(); std::cout << "opt value is: " << val << std::endl; @@ -130,9 +130,9 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max) d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, true); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); // expect the maxmum x = ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(), @@ -154,9 +154,9 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary) d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); // expect the maximum x = 18 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(), |