Assertion Violation at ../src/ast/array_decl_plugin.cpp:318

[brutalsavage]

Description: ASSERTION VIOLATION (UNEXPECTED CODE WAS REACHED) with array-ext

small code small.smt2 to reproduce:

(declare-const arr1 (Array Int Int))
(declare-const arr2 (Array Int Int))

(assert (= (div (array-ext 0 arr2) 4) (* (div (array-ext 0 arr1) 4) 2)))

output

ASSERTION VIOLATION
File: ../src/ast/array_decl_plugin.cpp
Line: 318
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
A

Command: running z3 (6c24a70) with debug build z3 small.smt2