Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Bug with length of "#x...." defined BVs #442

Closed
cdmcdonell opened this issue Sep 29, 2017 · 1 comment
Closed

Bug with length of "#x...." defined BVs #442

cdmcdonell opened this issue Sep 29, 2017 · 1 comment
Assignees
@marcogario
Labels
bug
Milestone
0.7.5

Comments

@cdmcdonell
Copy link

cdmcdonell commented Sep 29, 2017 •
edited

This appears to be a long-standing bug:


diff --git a/pysmt/smtlib/parser/parser.py b/pysmt/smtlib/parser/parser.py
index 487f26c..c9aed67 100644
--- a/pysmt/smtlib/parser/parser.py
+++ b/pysmt/smtlib/parser/parser.py
@@ -619,7 +619,7 @@ class SmtLibParser(object):
                     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:
@marcogario marcogario self-assigned this Sep 30, 2017
@marcogario marcogario added the bug label Oct 1, 2017
@marcogario marcogario added this to the 0.7.5 milestone Oct 1, 2017
marcogario added a commit that referenced this issue Oct 1, 2017
@marcogario
Bugfix: SMTLIB Parsing #x BV constants
17c228f 
SMT-LIB parsing of bv constants using the hexadecimal syntax
(e.g., #x10) would leads to the incorrect width of the bit-vector.

Fixes issue #442. Thanks to @cdmcdonell for reporting this.
@marcogario marcogario mentioned this issue Oct 1, 2017
Merged
@marcogario
Copy link
Contributor

Thank you for reporting this. See PR #443.

@mikand mikand mentioned this issue Oct 17, 2017
Closed
nbailluet pushed a commit to nbailluet/pysmt that referenced this issue Mar 14, 2024
@marcogario
Bugfix: SMTLIB Parsing #x BV constants
f76bcf3 
SMT-LIB parsing of bv constants using the hexadecimal syntax
(e.g., #x10) would leads to the incorrect width of the bit-vector.

Fixes issue pysmt#442. Thanks to @cdmcdonell for reporting this.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@marcogario marcogario

Labels
bug
Projects
None yet
Milestone
0.7.5
Development

No branches or pull requests
2 participants
@marcogario @cdmcdonell