Tests: Add test for issue #435

pysmt/formula.py

@@ -569,7 +569,7 @@ def BV(self, value, width=None):
         if width is None:
             raise PysmtValueError("Need to specify a width for the constant")
 
-        if is_python_integer(value):
+        if is_python_integer(value): # Account for various types if Integer
             if value < 0:
                 raise PysmtValueError("Cannot specify a negative value: %d" \
                                       % value)

pysmt/test/__init__.py

@@ -24,6 +24,7 @@
     import unittest
 
 from pysmt.environment import get_env, reset_env
+skipIf = unittest.skipIf
 
 
 class TestCase(unittest.TestCase):

pysmt/test/test_bv.py

@@ -15,12 +15,15 @@
 #   See the License for the specific language governing permissions and
 #   limitations under the License.
 #
-from pysmt.test import TestCase, skipIfNoSolverForLogic, main
+
+from pysmt.test import TestCase, skipIfNoSolverForLogic, skipIf, main
 from pysmt.shortcuts import Symbol, And, Symbol, Equals, TRUE
 from pysmt.shortcuts import is_sat, is_valid, get_model, is_unsat
 from pysmt.typing import BVType, BV32, BV128
 from pysmt.logics import QF_BV
 from pysmt.exceptions import PysmtValueError, PysmtTypeError
+from pysmt.constants import USE_GMPY
+
 
 class TestBV(TestCase):
 
@@ -307,5 +310,18 @@ def test_is_bv_constant(self):
         self.assertFalse(bvconst.is_bv_constant(3,9))
         self.assertFalse(bvconst.is_bv_constant(3))
 
+    @skipIf(not USE_GMPY, "Not using GMPY")
+    def test_bv_from_gmpy(self):
+        """BV constructor performs conversion if the constant is a GMPY"""
+
+        from pysmt.constants import pysmt_integer_from_integer
+        mgr = self.env.formula_manager
+        five = pysmt_integer_from_integer(5)
+        const5 = mgr.BV(five, 32)
+        const5b = mgr.BV(5, 32)
+        self.assertIsNotNone(const5)
+        self.assertEqual(const5, const5b)
+
+
 if __name__ == "__main__":
     main()