Help on error "# BMC: SAT Solver failed, try again" when runing arbiter example

From: Li, Lun (lli_at_mail.smu.edu)
Date: Fri Aug 26 2005 - 11:56:32 MDT

• Next message: Bing.Li_at_colorado.edu: "Fwd: Re: Help on error "# BMC: SAT Solver failed, try again" when runing arbiter example"
• Previous message: Osama Neiroukh: "VIS and "AllSAT""
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ] [ attachment ]
• Mail actions: [ respond to this message ] [ mail a new topic ]

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>

• application/ms-tnef attachment: winmail.dat

• Next message: Bing.Li_at_colorado.edu: "Fwd: Re: Help on error "# BMC: SAT Solver failed, try again" when runing arbiter example"
• Previous message: Osama Neiroukh: "VIS and "AllSAT""
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ] [ attachment ]
• Mail actions: [ respond to this message ] [ mail a new topic ]

This archive was generated by hypermail 2.1.7 : Fri Aug 26 2005 - 12:02:53 MDT