team-worthwhile/worthwhile — Issue #83: SMTLIB: When modifying an array index the old and new array do not not equal
Author: bafain
Created: 2012-02-20 18:58:50+00:00
State: open
Labels: prover

This is either my misunderstanding of the [SMTLIB array theory](http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2) or an error in Z3's implementation of it, because:

(assert (= (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) (store (store ((as const (Array Int Int)) 0) 0 1) 1 2)))
(check-sat)
sat

but

(assert (= (select (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 0) (select (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0)))
(check-sat)
unsat