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.

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

create_z3_var_typed shall be used throughout the code #60

Open
jlvargasme opened this issue Sep 3, 2022 · 0 comments
Open

create_z3_var_typed shall be used throughout the code #60

jlvargasme opened this issue Sep 3, 2022 · 0 comments

Comments

@jlvargasme
Copy link
Collaborator

jlvargasme commented Sep 3, 2022

Past prototyping used create_z3_var when the type was unknown and this caused many variables to be assumed "float" type. This is the source of many z3(type error) exceptions.

We should replace all the occurrences of create_z3_var with create_z3_var_typed or any other function that will give the correct type to a z3 variable.

For an example, see the create_base_var_from_pattern function that uses pattern matching in a Zelus pattern construct to figure out base type and variable name.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant