Assertion violation: File: ../src/util/old_vector.h Line: 370 idx < size()

[wintered]

Hi,

The following formula throws an assertion violation when using z3 with smt.arith.solver=1 option.

(declare-fun a () Int)
(declare-fun b () Int)
(assert (<= 0 a))
(declare-fun c (Int) Bool)
(declare-fun ab (Int) Int)
(declare-fun j (Int) Bool)
(declare-fun ac (Int) Int)
(push)
(assert (= (= 0 1) (j 0)))
(assert (= (ac 0) (ite (= b 0) (ab 0) 0)))
(assert (not (j 0)))
(assert (let ((az (not (c 0)))) (and az az)))
(check-sat)

ASSERTION VIOLATION
File: ../src/util/old_vector.h
Line: 370
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Revision: 28cb13f