Riddle: one car in three boxes. Possible SMT-Lib solution

game.smt2

; There are 3 boxes, exactly one of which has a car. You can keep the car if you pick the correct box!
;
; On each box there is a statement, exactly one of which is true.
;
; Box 1: The car is in this box. 
; Box 2: The car is not in this box. 
; Box 3: The car is not in box 1.
;
; Possible answers:
; - Box 1
; - Box 2
; - Box 3
; - None of them
; - Not enough information

; position of the car:
(declare-const x Bool) ; car in box 1
(declare-const y Bool) ; car in box 2
(declare-const z Bool) ; car in box 3

; truth of the statements
(declare-const a Bool) ; stmt 1 is true
(declare-const b Bool) ; stmt 2 is true
(declare-const c Bool) ; stmt 3 is true

(define-fun excl ((u Bool) (v Bool) (w Bool)) Bool
  (=> u (and (not v) (not w)))) ; if u is true then v and w must be false
  
(define-fun one ((u Bool) (v Bool) (w Bool)) Bool
  (and (excl u v w) ; u excludes the others
       (excl v u w) ; v excludes the others
       (excl w u v) ; w excludes the others
       (or u v w))) ; at least one must be true

; (simplify (one a b c))

(assert (one a b c))
(assert (one x y z))

; encoding of the statements
(assert (iff a x))
(assert (iff b (not y)))
(assert (iff c (not x)))

(check-sat) ; sat expected
(get-model)

(assert (not y)) ; if uncommented it should be unsat
(check-sat) ; unsat expected: previous solution is unique

(exit)

There are 3 boxes, exactly one of which has a car. You can keep the car if you pick the correct box!

On each box there is a statement, exactly one of which is true.

• Box 1: The car is in this box.
• Box 2: The car is not in this box.
• Box 3: The car is not in box 1.

Which box has the car?

• Box 1
• Box 2
• Box 3
• None of them
• Not enough information

Encoding pseudo-boolean with Int:

(define-fun pbool ((x Int)) Bool
  (or (= x 0) (= x 1)))

; positions: box 1, 2, 3
(declare-const x Int) (assert (pbool x))
(declare-const y Int) (assert (pbool y))
(declare-const z Int) (assert (pbool z))

; label sentences of box 1, 2, 3
(declare-const a Int) (assert (pbool a))
(declare-const b Int) (assert (pbool b))
(declare-const c Int) (assert (pbool c))

(assert (= 1 (+ a b c)))
(assert (= 1 (+ x y z)))

(assert (= a x))
(assert (= b (- 1 y)))
(assert (= c (- 1 x)))

(check-sat) ; sat expected
(get-model)

(assert (= y 0)) ; if uncommented it should be unsat
(check-sat) ; unsat expected

(exit)

Expected result:

sat
(model 
  (define-fun z () Int
    0)
  (define-fun y () Int
    1)
  (define-fun a () Int
    0)
  (define-fun c () Int
    1)
  (define-fun x () Int
    0)
  (define-fun b () Int
    0)
)
unsat

Shorter:

(declare-const box Int)
(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)

(assert (not (and a b)))
(assert (not (and a c)))
(assert (not (and b c)))

(assert (= a (= box 1)))
(assert (= b (not (= box 2))))
(assert (= c (not (= box 1))))
(check-sat)
(get-model)