Late setting simplifier elim-unconstrained leads to invalid sat result and model, and a segmentation fault #7647

superaxander · 2025-05-13T12:57:19Z

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.

The text was updated successfully, but these errors were encountered:

* add prd Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * missing text Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #7647 * fix #7647 - with respect to scope level --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add prd Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * missing text Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #7647 * fix #7647 - with respect to scope level * initial stab at randomizer Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Create prd.yml * missing text Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Update prd.yml * allows setting simplifier factory independently of whether solver has been allocated. Instances, such as #7484 can be solved faster by either having authors rewrite benchmarks or by using incremental pre-processing. You can add incremental pre-processing to the SMT solver by using the command ``` (set-simplifier (then simplify propagate-values solve-eqs elim-unconstrained simplify)) ``` This command can be invoked any time prior to push or adding assertions. The effect of the command is that it adds an incremental pre-processing pass to check-sat invocations that is potentially more powerful than the default pre-processing. The default pre-processing functionality is not touched mainly to avoid instability against functionality that is already built around its behavior. * remove experiment from pr --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

NikolajBjorner added a commit that referenced this issue May 17, 2025

fix #7647

3fac441

NikolajBjorner added a commit that referenced this issue May 17, 2025

fix #7647 - with respect to scope level

b0c8a5c

NikolajBjorner closed this as completed May 17, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Late setting simplifier elim-unconstrained leads to invalid sat result and model, and a segmentation fault #7647

Late setting simplifier elim-unconstrained leads to invalid sat result and model, and a segmentation fault #7647

Late setting simplifier elim-unconstrained leads to invalid sat result and model, and a segmentation fault #7647

Late setting simplifier elim-unconstrained leads to invalid sat result and model, and a segmentation fault #7647

Comments

Uh oh!