Merge pull request #395 from pysmt/boolector-assumptions-fix

Boolector Assumptions Fix

pysmt/solvers/btor.py

@@ -117,10 +117,8 @@ def get_model(self):
     @clear_pending_pop
     def _solve(self, assumptions=None):
         if assumptions is not None:
-            assumption = self.mgr.And(assumptions)
-            self._assert_is_boolean(assumption)
-            btor_assumption =  self.converter.convert(assumption)
-            self.btor.Assume(btor_assumption)
+            btor_assumptions = [self.converter.convert(a) for a in assumptions]
+            self.btor.Assume(*btor_assumptions)
 
         res = self.btor.Sat()
         if res == self.btor.SAT:

pysmt/test/test_regressions.py

@@ -20,7 +20,7 @@
 
 import pysmt.logics as logics
 import pysmt.smtlib.commands as smtcmd
-from pysmt.shortcuts import (Real, Plus, Symbol, Equals, And, Bool, Or,
+from pysmt.shortcuts import (Real, Plus, Symbol, Equals, And, Bool, Or, Not,
                              Div, LT, LE, Int, ToReal, Iff, Exists, Times, FALSE,
                              BVLShr, BVLShl, BVAShr, BV, BVAdd, BVULT, BVMul,
                              Select, Array)
@@ -419,6 +419,17 @@ def test_git_version(self):
         parts = v.split("-")
         self.assertTrue(len(parts) , 4)
 
+    @skipIfSolverNotAvailable("btor")
+    def test_boolector_assumptions(self):
+        with Solver(name='btor') as solver:
+            x = Symbol('x')
+            y = Symbol('y')
+            solver.add_assertion(Or(x, y))
+            solver.solve([Not(x), Not(y)])
+            btor_notx = solver.converter.convert(Not(x))
+            btor_noty = solver.converter.convert(Not(y))
+            self.assertEqual(solver.btor.Failed(btor_notx, btor_noty),
+                             [True, True])
 
 if __name__ == "__main__":
     main()