Storing mechanisms in Z3 SMT solver

Question

Here I'm attaching one piece of code as an input to Z3 online version. Is there any way to get 4 test cases as output of z3. When I give it to z3, it shows only one testcase at a time, otherwise shows unsat and no model available. Is there any solution for the above problem? Will all assertions work at the same time and give output like answer equals 1,2,3,4? adding (check-sat)and (get-value(answer))after each assertions again shows the output as answer is 1.other three cases are unsat.I want output like answer=1,answer=2,answer=3,answer=4 for this code,can you help me?

(declare-const answer Int) 
(assert (= answer 1) ) 
(check-sat)
(get-value(answer))
(assert (and ( not ( = answer 1 ) ) (= answer 2)) ) 
(check-sat)
(get-value(answer))
(assert (and ( and ( not ( = answer 2 ) ) ( not ( = answer 1 ) ) ) (= answer 3)) ) 
(check-sat)
(get-value(answer))
(assert (and ( and ( and ( not ( = answer 3 ) ) ( not ( = answer 2 ) ) ) ( not ( = answer 1 ) ) ) (= answer 4)) ) 
(check-sat)
(get-value(answer))

Answer 1

You can issue

(check-sat)
(get-value (answer))

as many times as you like; interleaving it with your assertions. Any time you call it, it'll check all the assertions so far.

There are also ways to "forget" previous assertions, but it doesn't seem like that's what you're after. For details on the SMTLib command language, see: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf, Section 3.9.

I'm not sure why you tagged your question with Python, as this is clearly an SMTLib question. If you're using the z3py interface, then you can do very similar things there as well by calling s.check() multiple times after declaring s as a Solver.