[YICES] Logical context is inconsistent

Bruno Dutertre bruno at csl.sri.com
Wed Oct 12 15:07:09 PDT 2011


Yu Huang wrote:
> Thanks!
> 
> So, what is the different between unsat and unsat Logical context is
> inconsistent.  What distinguishes these two messages?
> 

"unsat" is printed as the result of (check)

"Logical context is inconsistent. Use (reset) to reset." is printed as
an error message when you try to do something that cannot be done in an
inconsistent context. Examples: more (assert ...) or (check) or (push)...

Sometimes, Yices can determine that an assertion contradicts
whatever has been asserted before. It will then print "unsat"
after the assertion, and before (check).

Here's a simple example:

(define a::int)
(assert (> a 0))
(assert (not (> a 0))
--> unsat
(check)
--> Logical context is inconsistent.


Bruno



More information about the YICES mailing list