(bv) Segmentation fault (release) or Assertion violation at ../src/ast/ast.cpp Line: 1929

[muchang]

Hi,
For this case, Z3 throws out a segmentation fault:

[113] % ./z3debug small.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 1929
m_ast_table.contains(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
A
[113] % ./z3release small.smt2 
unknown
[1]    70788 segmentation fault  ./z3release small.smt2
[114] % cat small.smt2 
(declare-sort a) 
(declare-sort b) 
(declare-sort c) 
(declare-sort d) 
(declare-sort n) 
(declare-fun e (b Int) a) 
(declare-fun f () b) 
(declare-fun o (c a) Int) 
(declare-fun g () c) 
(declare-fun h (d Int) Int) 
(declare-fun i () d) 
(declare-fun j (n Int) c) 
(declare-fun k () n) 
(assert (= 0   (o (j k 0) (e f 2)))) 
(assert (forall ((?l Int)) (let ((?m (e f 2))) (= (o (j k (h i ?l)) ?m) 0)))) 
(assert (forall ((?l Int)) (let ((?m (o (j k ?l) (e f 2)))) (= (h i ?m) ?m)))) 
(assert (forall ((?l Int)) (= (o g (e f ?l)) 0))) 
(check-sat-using bv)                                                                                                                
[115] %

OS: Ubuntu 18.04
Commit: 7f1b147