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

Assertion violation at /src/ast/ast.h #6174

Closed
merlinsun opened this issue Jul 19, 2022 · 0 comments
Closed

Assertion violation at /src/ast/ast.h #6174

merlinsun opened this issue Jul 19, 2022 · 0 comments

Comments

@merlinsun
Copy link

Hi,
For this instance, z3 dead0c9 debug build

# z3 small.smt2
sat
sat
ASSERTION VIOLATION
File: ../src/ast/ast.h
Line: 937
is_app(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
 
# cat small.smt2
(set-option :rewriter.expand_nested_stores true)
(declare-const x27 Bool)
(declare-const x (Array (Array (Array Bool Bool) (Array Bool Bool)) (Array (Array Bool Bool) Bool)))
(declare-const x2 Bool)
(declare-fun a () (Array Bool Bool))
(declare-fun ar () (Array (Array Bool Bool) Bool))
(declare-fun r5 () (Array (Array Bool Bool) (Array Bool Bool)))
(check-sat)
(assert (exists ((V Int)) true))
(check-sat)
(assert (or x2 x27))
(assert (forall ((r (Array (Array Bool Bool) (Array Bool Bool)))) (and x2 (= (store x r (store ar a true)) (store (store x r5 ar) r ar)))))
(check-sat)
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