search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.22k stars 1.47k forks source link

Questions about the combination of quantitative formulas #7276

Closed Heaven2024 closed 2 months ago

Heaven2024 commented 3 months ago

I tried to solve the two formulas separately

(declare-const x (Array Int Int))
(declare-const y (Array Int Int))
(declare-fun a () (Array Int Int))
(assert (forall ((v (Array (Array Int Int) Real))) (= 0.0 (select (store v x 0.0) a))))
(check-sat)
(declare-const x (Array Int Int))
(declare-const y (Array Int Int))
(declare-fun a () (Array Int Int))
(assert (forall ((w (Array (Array Int Int) Real))) (= 0.0 (select (store w y 0.0) a))))
(check-sat)

Both return sat when combined:

(declare-const x (Array Int Int))
(declare-const y (Array Int Int))
(declare-fun a () (Array Int Int))
(assert (forall ((v (Array (Array Int Int) Real))) (= 0.0 (select (store v x 0.0) a))))
(assert (forall ((w (Array (Array Int Int) Real))) (= 0.0 (select (store w y 0.0) a))))
(check-sat)

it return unknown

NikolajBjorner commented 2 months ago

it can be solved with (set-option :sat.euf true)