mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

fix crash

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-25 13:41:57 -07:00 • committed by Arie Gurfinkel
parent a8438e081e
commit e6401908a5
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/qe/qe_arrays.cpp
View file

@ -802,8 +802,9 @@ namespace qe {
*/ */
expr* reduce_core (app *a) { expr* reduce_core (app *a) {
if (!m_arr_u.is_store (a->get_arg (0))) return a; if (!m_arr_u.is_store (a->get_arg (0))) return a;
unsigned arity = get_array_arity(m.get_sort(a)); expr* array = a->get_arg(0);
expr* array = a->get_arg (0); unsigned arity = get_array_arity(m.get_sort(array));
expr* const* js = a->get_args() + 1; expr* const* js = a->get_args() + 1;
while (m_arr_u.is_store (array)) { while (m_arr_u.is_store (array)) {