Skip to content

Commit

Permalink
Fixed failing test on get_model by specifying the expected logic.
Browse files Browse the repository at this point in the history
  • Loading branch information
marcogario committed Feb 25, 2015
1 parent d7de41f commit ed99be4
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions pysmt/test/test_solving.py
Original file line number Diff line number Diff line change
Expand Up @@ -70,10 +70,10 @@ def test_get_model_unsat(self):
f = And(varA, Not(varB))
g = f.substitute({varB:varA})

res = get_model(g)
res = get_model(g, logic=QF_BOOL)
self.assertIsNone(res, "Formula was expected to be UNSAT")

for solver in get_env().factory.all_solvers():
for solver in get_env().factory.all_solvers(logic=QF_BOOL):
res = get_model(g, solver_name=solver)
self.assertIsNone(res, "Formula was expected to be UNSAT")

Expand All @@ -84,12 +84,12 @@ def test_get_model_sat(self):

f = And(varA, Equals(varX, Real(8)))

res = get_model(f)
res = get_model(f, logic=QF_LRA)
self.assertIsNotNone(res, "Formula was expected to be SAT")
self.assertTrue(res.get_value(varA) == TRUE())
self.assertTrue(res.get_value(varX) == Real(8))

for solver in get_env().factory.all_solvers():
for solver in get_env().factory.all_solvers(logic=QF_LRA):
res = get_model(f, solver_name=solver)
self.assertIsNotNone(res, "Formula was expected to be SAT")
self.assertTrue(res.get_value(varA) == TRUE())
Expand Down

0 comments on commit ed99be4

Please sign in to comment.