[YICES] Logical context is inconsistent

Yu Huang goyu86 at gmail.com
Wed Oct 12 15:00:00 PDT 2011


1. So, what is the different between unsat and unsat Logical context
is inconsistent.  What distinguishes these two messages?

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?
Thanks for answering!

First scenario:                            Second scenario:

(define A::int)                              (define A::int)
(define B::int)                              (define B::int)
		
(assert (= A 1))                           (assert (= A 1))
(assert (= B 1))                           (assert (= B 1))

(assert (and (< A B) (/= A B)))      (assert (< A B))
                                                 (assert (/= A B))

(check)                                      (check)


Yours,
Yu



On Wed, Oct 12, 2011 at 3:42 PM, Yu Huang <goyu86 at gmail.com> wrote:
> Thanks!
>
> So, what is the different between unsat and unsat Logical context is
> inconsistent.  What distinguishes these two messages?
>
>
> Yours,
> Yu Huang
>
>
>
>
>
> On Mon, Sep 19, 2011 at 10:29 AM, Bruno Dutertre <bruno at csl.sri.com> wrote:
>> Yu Huang wrote:
>>>
>>> Hi, folks,
>>>
>>> I am now working on solving SMT problem for multi-thread program by
>>> using Yices. It reports the message "Logical context is inconsistent".
>>> I wonder what it means. Thanks!
>>>
>>>
>>> Yu
>>>
>>
>> Yu,
>>
>> Yices prints this message when it knows that the set
>> of assertions you've given is no satisfiable.
>>
>> Bruno
>>
>



More information about the YICES mailing list