Assertion violation at File: ../src/ast/ast.h Line: 952

[merlinsun]

Hi,
For this instance, z3 965bee5 debug build

$ 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

[NikolajBjorner]

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).