Strategies for coping with no instance found?

Do people have any heuristics or strategies for coping with the dreaded “no instance found”? Obviously, one answer is to step incrementally, versioning along the way, but presumably there are times when one has to work with other peoples’ specs.

(And, incidentally, sometimes it appears that an answer is to restart Alloy.)

If you’re on Mac or Linux, you have access to Minisat’s Unsat Core, which will highlight the predicates that lead to “no instance found”. See here:

1 Like

Ah, but not in the standard download for Electrum. :cry:

Anyone got instructions for setting it up?

Thx all


I think the unsat core is already working properly in the latest release candidate (2.1 RC4).


Just installed the jar, but I can’t see the Minisat in the menu. Is there something else I have to do?
Incidentally, after starting up, I get the message Mac classes not there

(Running on OS/X)

I am running electrum 2 rc 2 on MacOS, see the native solvers. Are you running on Java 8?

1 Like

Good catch. Forgot to set the local vm after a reboot (using jenv)