1

If one formula has more than one model, is there some way to print them?

I have a problem for which I know there are many solutions. However, if I use the following commands

(check-sat)
(get-model)
(check-sat)
(get-model)

z3 prints the same model twice, instead of giving me two different models.

Q: Is there any way to extract multiple, different, models of a formula?

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
Marin
  • 15
  • 2

1 Answers1

1

There's no automated way to do this. The usual trick is to assert the negation of the last model, and ask for another one.

See this answer for details: how to get multiple solutions for z3 solver in smt2 format example?

alias
  • 28,120
  • 2
  • 23
  • 40