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

Z3 doesn't handle some #Not (#Exists ...) predicates #3447

Open
ana-pantilie opened this issue Jan 18, 2023 · 0 comments · May be fixed by #3455
Open

Z3 doesn't handle some #Not (#Exists ...) predicates #3447

ana-pantilie opened this issue Jan 18, 2023 · 0 comments · May be fixed by #3455
Assignees
Labels

Comments

@ana-pantilie
Copy link
Contributor

High priority

Z3 is unable to refute predicates like:

#Not ( 
	#Exists ITER_COUNT_F:Int . 
		     { VV6__data_3c5818c8:Bytes [ 32 *Int ?ITER_COUNT_F:Int .. #sizeByteArray ( VV6__data_3c5818c8:Bytes ) -Int 32 *Int ?ITER_COUNT_F:Int ] #Equals VV6__data_3c5818c8:Bytes [ 32 *Int ITER_COUNT_F:Int .. #sizeByteArray ( VV6__data_3c5818c8:Bytes ) -Int 32 *Int ITER_COUNT_F:Int ] } 
		#And { true #Equals 0 <=Int ITER_COUNT_F:Int }
		#And { true #Equals 32 *Int ITER_COUNT_F:Int <Int #sizeByteArray ( VV6__data_3c5818c8:Bytes ) }
		#And { true #Equals #sizeByteArray ( VV6__data_3c5818c8:Bytes ) <=Int 32 *Int ITER_COUNT_F:Int +Int 32 }
		#And { true #Equals -9 <Int #sizeByteArray ( VV6__data_3c5818c8:Bytes ) } 
	)
...
#And { true #Equals 0 <=Int ?ITER_COUNT_F:Int }
#And { true #Equals 32 *Int ?ITER_COUNT_F:Int <Int #sizeByteArray ( VV6__data_3c5818c8:Bytes ) }
#And { true #Equals #sizeByteArray ( VV6__data_3c5818c8:Bytes ) <=Int 32 *Int ?ITER_COUNT_F:Int +Int 32 }
...

@PetarMax suggests a heuristic which looks for witnesses in the free variables of the predicate.

@ana-pantilie ana-pantilie self-assigned this Jan 18, 2023
@ana-pantilie ana-pantilie linked a pull request Jan 23, 2023 that will close this issue
4 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant