Arithmetic operation with Boolean values

[rodrigo7491]

Z3 returns unsat for the instance below, which contains a subtraction involving an Int and a Bool variable, (- F B).

(set-logic QF_LIA)

(define-fun state ((A Bool) (B Bool) (C Bool) (D Bool) (E Int) (F Int) (G Int) (H Int)) Bool (or (or (or (or (or (or (or (or (or (or (or (or (and (and (and (and (= A true) (= C true)) (= D true)) (not (= B true))) (>= F 1)) (and (and (and (= A true) (= C true)) (and (not (= B true)) (not (= D true)))) (and (>= F 1) (>= H 1)))) (and (and (and (= A true) (= C true)) (not (= D true))) (and (and (>= (- F B) 1) (>= F 1)) (>= H 1)))) (and (and (and (= A true) (= D true)) (and (not (= B true)) (not (= C true)))) (and (>= F 1) (>= H 1)))) (and (and (and (= C true) (= D true)) (and (not (= A true)) (not (= B true)))) (and (>= F 1) (>= H 1)))) (and (and (and (= C true) (= D true)) (not (= A true))) (and (and (>= (- F B) 1) (>= F 1)) (>= H 1)))) (and (and (= C true) (and (and (not (= A true)) (not (= B true))) (not (= D true)))) (>= F 1))) (and (and (= C true) (and (not (= A true)) (not (= D true)))) (and (>= (- F B) 1) (>= F 1)))) (and (and (= D true) (and (and (not (= A true)) (not (= B true))) (not (= C true)))) (and (>= F 1) (>= H 1)))) (and (and (= D true) (and (not (= A true)) (not (= C true)))) (and (and (>= (- F B) 1) (>= F 1)) (>= H 1)))) (and (and (not (= A true)) (not (= C true))) (not (= D true)))) (and (and (not (= B true)) (not (= C true))) (not (= D true)))) (and (and (not (= C true)) (not (= D true))) (and (>= (- F B) 1) (>= F 1)))))

(declare-fun A ()  Bool)
(declare-fun B ()  Bool)
(declare-fun C ()  Int)
(declare-fun D ()  Int)
(declare-fun E ()  Int)
(declare-fun F ()  Int)
(declare-fun G ()  Bool)
(declare-fun H ()  Bool)

(assert
    (and
      (and (= A true) (not H) (not G) (not B))
      (not (state B A H G F E D C))
    )
)

(check-sat)
(exit)

It is unclear to me if Z3 encodes Booleans as integers, like Eldarica (see uuverifiers/eldarica#51), or if this is an edge case. I was not able to reproduce the behaviour with a toy example.

[NikolajBjorner]

YOu can see the state by replacing (check-sat) by (apply simplify)

(apply simplify)
;(check-sat)
(exit)

z3 6719.smt2 -v:10
(simplifier :num-exprs 86 :num-asts 419 :time 0.03 :before-memory 17.25 :after-memory 17.35)
(goals
(goal
  A
  (not H)
  (not G)
  (not B)
  (not (and B H G (not A) (>= E 1)))
  (not (and B H (not A) (not G) (>= E 1) (>= C 1)))
  (let ((a!1 (>= (+ E (* (- 1) (ite A 1 0))) 1)))
    (not (and B H (not G) a!1 (>= E 1) (>= C 1))))
  (not (and B G (not A) (not H) (>= E 1) (>= C 1)))
  (not (and H G (not B) (not A) (>= E 1) (>= C 1)))
  (let ((a!1 (>= (+ E (* (- 1) (ite A 1 0))) 1)))
    (not (and H G (not B) a!1 (>= E 1) (>= C 1))))
  (not (and H (not B) (not A) (not G) (>= E 1)))
  (let ((a!1 (>= (+ E (* (- 1) (ite A 1 0))) 1)))
    (not (and H (not B) (not G) a!1 (>= E 1))))
  (not (and G (not B) (not A) (not H) (>= E 1) (>= C 1)))
  (let ((a!1 (>= (+ E (* (- 1) (ite A 1 0))) 1)))
    (not (and G (not B) (not H) a!1 (>= E 1) (>= C 1))))
  (not (and (not B) (not H) (not G)))
  (not (and (not A) (not H) (not G)))
  (let ((a!1 (>= (+ E (* (- 1) (ite A 1 0))) 1)))
    (not (and (not H) (not G) a!1 (>= E 1))))
  :precision precise :depth 1)
)

It uses unit propagation simplification to establish unsat.