[YICES] Logical context is inconsistent

[Bruno Dutertre]

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".

It's either

"unsat" as a result of the command

or

"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
> difference?

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,

Bruno