jrh13 / hol-light

The HOL Light theorem prover
Other
435 stars 79 forks source link

Augment CADICAL_PROVE to raise Satisfiable if counterexample exists #104

Closed aqjune closed 3 months ago

aqjune commented 4 months ago

This is a small patch to update CADICAL_PROVE raise "Satisfiable" failure if the query has a counterexample. This is useful when the user wants to know whether the query's failure is either from limited resource or because it is logically false.