Late setting simplifier elim-unconstrained leads to invalid sat result and model, and a segmentation fault #7647
Description
I noticed that Z3 (tested on version 4.15.0 and 4.12.5) produced a wrong result/model for the following input:
(set-option :smt.auto-config false)
(set-option :produce-models true)
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const l Int)
(declare-const r Int)
(assert (<= 0 a))
(assert (<= a 7))
(assert (<= 0 b))
(assert (<= b 7))
(assert (= l (bv2nat (bvand ((_ int2bv 3) a) ((_ int2bv 3) b)))))
(assert (= r (div (bv2nat (bvxor ((_ int2bv 3)a) ((_ int2bv 3) b))) 2)))
(assert (= c (+ l r)))
(push)
(set-simplifier elim-unconstrained)
(assert (not (= c (div (+ a b) 2))))
(check-sat)
(get-model)
(pop)This yields:
sat
(
(define-fun l () Int
0)
(define-fun c () Int
1)
(define-fun a () Int
0)
(define-fun r () Int
1)
(define-fun b () Int
2)
)
zsh: segmentation fault (core dumped)Whereas the expected result is unsat since c = (a + b) / 2. Removing the (set-simplifer elim-unconstrained) yields unsat and no crash.
Reducing this further the following program also causes a segmentation fault:
(push)
(set-simplifier elim-unconstrained)
(pop)Setting the simplifier at the start of the file anywhere on the top level does not cause these issues. The segmentation fault does not happen until the (pop) (or when the file ends).
I suppose it is simply not allowed to set the simplifier if you're not on the top level? Even still I've only been able to replicate the invalid (check-sat) result when using elim-unconstrained.