Re: [SLAM] Question regarding finding predicates 1 Prgramm

From: Ayrat <ayrat.khalimov ***AT***iaik.tugraz.at>
Date: Thu, 5 Jan 2017 16:27:55 +0100
Subject: Re: [SLAM] Question regarding finding predicates 1 Prgramm
Newsgroups: tu-graz.lv.vt
Organization: Technische Universitaet Graz
Message-id: <cb46d672-bee7-beb4-9358-f6f8d5ee9f21@iaik.tugraz.at>
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1
References: <o4jqaq$11m$1@news.tugraz.at>
hi David,

Double check:

-  Is this the shortest CEX?
-  During the CEX analysis:
   if some predicate becomes false,
   then
   1) you take it as a new predicate.
   2) you trace the "history" of that predicate
      (to the point where it was introduced with "assume"),
       and add all the predicates that it was  before it became false.


good luck,
Ayrat

On 2017-01-04 10:43 PM, David Marogy wrote:
Hi,
dont know if i am missunderstanding something, but we should find
two predicates with one counterexample is this true?

Because i am just finding one if we go into the "else" part. Am i
overlooking something?

Would be nice if somebody has some tips for me.

Best regards,
David