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

fixed possible undefined variable assigment #6985

Merged
merged 1 commit into from
Nov 10, 2023

Conversation

EyalBrilling
Copy link
Contributor

On line 5690

n2 = n3

n3 gets a value on line 5657 only if is_zero is false.
On occurences where is_zero is true, n3 keeps its undefined value, potentially effecting n2 and the the rest of the calculations.
Simple fix of defining n3 = 0 - not effecting other calculations if value stays on 0 as it is only used in a '-' operation as the subtrahend.

@NikolajBjorner
Copy link
Contributor

Did you use a tool or do you not have a life?
In any case pretty cool. There are some long standing issues with nlsat, possibly not related to unintialized variables but likely require algorithmic understanding. See github issue tracker for nlsat tagged.

@EyalBrilling
Copy link
Contributor Author

I used clang static analyzer.
Will look at nlsat,thank you

@nadavrot
Copy link
Contributor

nadavrot commented Nov 9, 2023

@NikolajBjorner Can you please approve or reject @EyalBrilling's PR?

@NikolajBjorner NikolajBjorner merged commit aa9c791 into Z3Prover:master Nov 10, 2023
15 checks passed
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

Successfully merging this pull request may close these issues.

None yet

3 participants