[YICES] Logical context is inconsistent
bruno at csl.sri.com
Wed Oct 12 15:41:22 PDT 2011
Yu Huang wrote:
> 1. So, what is the different between unsat and unsat Logical context
> is inconsistent. What distinguishes these two messages?
As I wrote in my previous e-mail. There's no such thing as
"unsat Logical context is inconsistent".
"unsat" as a result of the command
"Logical context is inconsistent"
to inform you that the operation you want to perform is not
possible because the context is inconsistent.
> 2. Here are two "same" examples, in which the first example prints one
> message of logical inconsistence and the second one prints two
> messages of logical inconsistence. Why does yices make such
Try running Yices in interactive mode to see what happens.
Give option -i to the command line then type scenario 1 and
scenario 2 one command at a time. That should make it clear,
More information about the YICES