Not able to found how to get different solution after every boolector_sat under same assertions

[gsingla21]

Came across a BTOR_OPT_SEED option but it seems useless while running boolector_sat() multiple times. It shows the same result everytime. Want to get different result everytime boolector_sat() is executed through boolector_bv_assignment(). Is there any API that can I use to resolve it? I heard Picosat can enumerate all possible solutions without crutches. But how to get different or all possible sat solutions as output (could enumerate). I want to avoid extra assertions to negate the prev solution.

[aniemetz]

The seed passed via BTOR_OPT_SEED is internally only used for the local search engines, which are not enabled by default. Thus, it is expected that running boolector_sat() shows the same result every time. If you want to block models, you have to do this manually.