You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
$ cat small.smt2
(set-option :rewriter.expand_nested_stores true)
(declare-fun b ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int Int))
(declare-fun v () Int)
(declare-fun ar () (Array Int (Array Int Int)))
(declare-fun a () (Array Int (Array Int Real)))
(declare-fun r () (Array Int Int))
(assert (= (select (b a a) 0) (r v (r a))))
(assert (exists ((V Int)) (distinct r (store r 0 0))))
(assert (forall ((var20 Int)) (and (forall ((var20 (Array Int (Array Int Int)))) (= ar (store var20 0 (store (var20 0) 0 0)))))))
(check-sat-using qsat)
$ z3 small.smt2
(error "line 7 column 39: unknown constant r ((Array Int (Array Int Real)))
declared: (declare-fun r () (Array Int Int)) ")
ASSERTION VIOLATION
File: ../src/ast/ast.h
Line: 952
is_app(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
The text was updated successfully, but these errors were encountered:
not clear the overhead of fixing such a bug is worth while: it relies on setting parameters outside their default ranges that are incompatible with qsat assumptions and for domains where qsat isn't designed for (LIA/LRA/DT), with nlqsat for (NRA).
Hi,
For this instance, z3 965bee5 debug build
The text was updated successfully, but these errors were encountered: