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

Non well-founded datatype declaration randomly causes segfaults or malloc error #2504

Closed
tizmd opened this issue Aug 20, 2019 · 0 comments
Closed

Comments

@tizmd
Copy link

tizmd commented Aug 20, 2019

This datatype declaration, which should be rejected because it is not well-founded, causes
a segfault at sometime, a malloc error at another execution, or silently accepted by z3.

(declare-datatypes ( (|phi[0]| 1) (|phi[1]| 1) (|phi[2]| 1) (|phi[3]| 1) (|phi[4]| 1) (|phi[5]| 1) ) (
(par (X) ( (init (value X)))) 
(par (X) ( (phi-0 (val-0 (|phi[0]| X))) ))
(par (X) ( (phi-1 (val-1 (|phi[1]| X))) (phi-5 (val-5 (|phi[5]| X)))))
(par (X) ( (phi-2 (val-2 (|phi[2]| X))) ))
(par (X) ( (phi-3-4 (val-3-4 (|phi[3]| X))) ))
(par (X) ( (phi-3-5 (val-3-5 (|phi[3]| X))) ))
))

OS: Mac OS X 10.14.6
z3 version: 4.8.5 - 64 bit

$ z3 problematic.smt2 
z3(81229,0x10dae25c0) malloc: *** error for object 0x7fd961549800: pointer being freed was not allocated
z3(81229,0x10dae25c0) malloc: *** set a breakpoint in malloc_error_break to debug
Abort trap: 6
$ z3 problematic.smt2 
$ z3 problematic.smt2 
$ z3 problematic.smt2 
Segmentation fault: 11
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