From: Bing.Li_at_colorado.edu
Date: Fri Aug 26 2005 - 15:23:54 MDT
----- Forwarded message from Mohammad Awedh <Mohammad.Awedh_at_colorado.edu> -----
Date: Fri, 26 Aug 2005 15:17:14 -0600
From: Mohammad Awedh <Mohammad.Awedh_at_colorado.edu>
Reply-To: Mohammad Awedh <Mohammad.Awedh_at_colorado.edu>
Subject: Re: Help on error "# BMC: SAT Solver failed, try again" when runing
arbiter example
To: Bing.Li_at_colorado.edu
Bing,
VIS 2.0 is not compatible with zchaff (Version II) . The output format of
zchaff (Version II) is different from the
old zchaff. However, VIS 2.1 is compatible with zchaff (Version II).
Mohammad.
----- Original Message -----
From: <Bing.Li_at_colorado.edu>
To: <awedh_at_colorado.edu>
Sent: Friday, August 26, 2005 1:59 PM
Subject: Fwd: Help on error "# BMC: SAT Solver failed, try again" when
runing arbiter example
> Hi, Mohammad:
>
> Could you take a look of it?
>
> Thanks
>
> Bing
>
> ----- Forwarded message from "Li, Lun" <lli_at_mail.smu.edu> -----
> Date: Fri, 26 Aug 2005 12:56:32 -0500
> From: "Li, Lun" <lli_at_mail.smu.edu>
> Reply-To: vis-users_at_lists.colorado.edu
> Subject: Help on error "# BMC: SAT Solver failed, try again" when runing
> arbiter example
> To: vis-users_at_lists.colorado.edu
>
> Dear All,
>
> I try to run the arbiter example in the VIS release package for LTL model
> checking. then I got error shown at the end.
>
> I test the zchaff (Verion II) seperately on some cnf files and it works
> fine. Any suggestion is appreciated.
>
> Thanks ahead
>
> Lun
>
> vis release 2.0 (compiled 19-Nov-04 at 10:03 AM)
> vis> source check_script
> Warning: Model main may have a cyclic connection which involves variable
> ackA
> Formula: G(!((((ackA=1 * ackB=1) + (ackB=1 * ackC=1)) + (ackC=1 *
> ackA=1))))
> LTL formula is of type G(p)
> Apply BMC on counterexample of length >= 1 and <= 5 (+1)
> # BMC: SAT Solver failed, try again
> # BMC: SAT Solver failed, try again
> # BMC: SAT Solver failed, try again
> # BMC: SAT Solver failed, try again
> # BMC: SAT Solver failed, try again
> # BMC: no counterexample found of length up to 5
> # BMC: formula undecided
> -- bmc time = 0.28
> Formula: G((reqA=1 -> F(ackA=1)))
> General LTL BMC
> Apply BMC on counterexample of length >= 1 and <= 5 (+1)
> # BMC: SAT Solver failed, try again
> # BMC: SAT Solver failed, try again
> # BMC: SAT Solver failed, try again
> # BMC: SAT Solver failed, try again
> # BMC: SAT Solver failed, try again
> # BMC: formula undecided
> # BMC: no counterexample found of length up to 5
> -- bmc time = 0.46
> Formula: G((reqB=1 -> F(ackB=1)))
> General LTL BMC
> Apply BMC on counterexample of length >= 1 and <= 5 (+1)
> # BMC: SAT Solver failed, try again
> # BMC: SAT Solver failed, try again
> # BMC: SAT Solver failed, try again
> # BMC: SAT Solver failed, try again
> # BMC: SAT Solver failed, try again
> # BMC: formula undecided
> # BMC: no counterexample found of length up to 5
> -- bmc time = 0.46
> Formula: G((reqC=1 -> F(ackC=1)))
> General LTL BMC
> Apply BMC on counterexample of length >= 1 and <= 5 (+1)
> # BMC: SAT Solver failed, try again
> # BMC: SAT Solver failed, try again
> # BMC: SAT Solver failed, try again
> # BMC: SAT Solver failed, try again
> # BMC: SAT Solver failed, try again
> # BMC: formula undecided
> # BMC: no counterexample found of length up to 5
> -- bmc time = 0.43
> ** cmd error: unknown command 'ctime'
> ** cmd error: aborting 'source check_script'
> vis>
>
> ----- End forwarded message -----
>
>
>
----- End forwarded message -----
This archive was generated by hypermail 2.1.7 : Fri Aug 26 2005 - 15:27:59 MDT