Is it possible to encode conditional sat checks in Z3?

Question

Suppose I have the following problem (which I've made trivial to simplify my question)

;; declare variables
(declare-const X0 Int)
(assert (>= X0 0))
(assert (<= X0 1))
(declare-const X1 Int)
(assert (>= X1 0))
(assert (<= X1 1))
(declare-const X2 Int)
(assert (>= X2 0))
(assert (<= X2 1))

;; two sat checks
(push)
(assert (= (0 (+ X1 X2))))
(check-sat)
(pop)
(push)
(assert (= (0 (+ X1 X2 X3))))
(check-sat)
(pop)

What I would like to do is skip the second sat check if the first sat check is unsat/sat. Is it possible to do this? I believe I could do this if I used Z3 with python (run the sat check, get the result, and use a python if statement on the result to determine whether to run the second check), but I would like to do it with smt-lib. Is this (easily) possible?

Answer 1

No. SMTLib language (http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf) does not have any "control structures" for you to issue the sat checks based on a previous result.

The solution is to use a higher level API, that is available from any number of host languages such as C/C++/C#/O'Caml/Python/Java/Scheme/Haskell, where you can program this sort of interaction.