Skip to content
New issue

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

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

Already on GitHub? # to your account

Assertion violation at src/model/datatype_factory.cpp:175 #4812

Closed
wintered opened this issue Nov 22, 2020 · 0 comments
Closed

Assertion violation at src/model/datatype_factory.cpp:175 #4812

wintered opened this issue Nov 22, 2020 · 0 comments

Comments

@wintered
Copy link

[556] % z3-4.8.8 small.smt2
unknown
[557] % z3release small.smt2
Segmentation fault
[558] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/model/datatype_factory.cpp
Line: 175
!found_fresh_arg || !set->contains(new_value)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[559] % cat small.smt2
(declare-datatypes ((a 0) (b 0) (d 0) (u 0) (v 0) (f 0) (i 0) (j 0) (k 0) (l 0) (m 0) (n 0) (o 0) (p 0) (q 0) (r 0))
 (((b(b v))) (b) (b) (b) ((b(b v)) s) ((b(h a)) (t (g a))) (b) (b) (b) (b) (b) (b) (b) (b) (b) (b)))
(declare-fun c (f) a)
(assert (forall ((e f)) (= (c e) (g e) (h e))))
(check-sat)
[560] %

OS: Ubuntu 18.04
Commit: 065e065

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

No branches or pull requests

1 participant