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 error at smt_model_finder.cpp:2201 #4796

Closed
rainoftime opened this issue Nov 15, 2020 · 0 comments
Closed

Assertion error at smt_model_finder.cpp:2201 #4796

rainoftime opened this issue Nov 15, 2020 · 0 comments

Comments

@rainoftime
Copy link
Contributor

Hi, for the following formula, z3 49a0266

(set-logic AUFNIRA)
(set-option :rewriter.expand_nested_stores true)
(declare-fun i17 () Int)
(declare-fun arr0 () (Array Int Bool))
(check-sat)
(declare-fun arr1 () (Array Int Bool))
(assert (= (store arr0 467 true) (store (store (store arr0 467 false) i17 true) 0 (exists ((q12 (Array Bool Int)) (q13 Int) (q14 (Array Int Bool)) (q15 Bool) (q16 (Array Bool Int)) (q17 Bool) (q18 (Array Bool Int))) q17)) arr1 (store arr0 467 true) arr0))
(check-sat)

$ z3 xx.smt2 
sat
ASSERTION VIOLATION
File: ../src/smt/smt_model_finder.cpp
Line: 2201
is_lambda(curr)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
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