Permalink
Browse files

Merge pull request #443 from pysmt/i442/bv_const

Bugfix: SMTLIB Parsing #x BV constants
  • Loading branch information...
mikand committed Oct 1, 2017
2 parents e833db0 + 17c228f commit 35662f00367f07d398255e3f3d6ff5eb32c3f2a8
Showing with 9 additions and 1 deletion.
  1. +1 −1 pysmt/smtlib/parser/parser.py
  2. +8 −0 pysmt/test/test_regressions.py
@@ -619,7 +619,7 @@ def atom(self, token, mgr):
if token[1] != "x":
raise PysmtSyntaxError("Invalid bit-vector constant "
"'%s'" % token)
width = (len(token) - 2) * 16
width = (len(token) - 2) * 4
value = int("0" + token[1:], 16)
res = mgr.BV(value, width)
else:
@@ -462,6 +462,14 @@ def test_parse_exception(self):
self.assertEqual(ex.pos_info[0], 0)
self.assertEqual(ex.pos_info[1], 19)
def test_parse_bvconst_width(self):
smtlib_input = "(assert (> #x10 #x10))"
parser = SmtLibParser()
buffer_ = cStringIO(smtlib_input)
expr = parser.get_script(buffer_).get_last_formula()
const = expr.args()[0]
self.assertEqual(const.bv_width(), 8, const.bv_width())
if __name__ == "__main__":
main()

0 comments on commit 35662f0

Please sign in to comment.