Re: Can't run check_invariant -A4 (The puresat algorithm)

From: Andrea Fedeli (andrea.fedeli_at_mclink.it)
Date: Fri Mar 30 2007 - 16:15:42 MDT

Next message: Zaher S Andraus: "Re: Can't run check_invariant -A4 (The puresat algorithm)"
Previous message: Zaher S Andraus: "Can't run check_invariant -A4 (The puresat algorithm)"
In reply to: Zaher S Andraus: "Can't run check_invariant -A4 (The puresat algorithm)"
Next in thread: Zaher S Andraus: "Re: Can't run check_invariant -A4 (The puresat algorithm)"
Reply: Zaher S Andraus: "Re: Can't run check_invariant -A4 (The puresat algorithm)"
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ] [ attachment ]
Mail actions: [ respond to this message ] [ mail a new topic ]

HI Zaher,

Zaher S Andraus wrote:

>
> Hi,
>
> VIS seems to function correctly w/ the default model checking
> mode, or with -A3 (Grab algorithm). I am having a problem with
> the -A4 option (PureSAT algorithm). VIS is crashing.

[...]

> Can anyone help?

I would need a bit of extra info from you:

1) The property file
2) The commands you executed.

With the information you gave it's not easy to dig into your issue.

Cheers,

Andrea.

-- 
Andrea Fedeli
A computer, to print out a fact,
Will divide, multiply, and subtract.
	But this output can be
	No more than debris,
If the input was short of exact.
		-- Gigo

Next message: Zaher S Andraus: "Re: Can't run check_invariant -A4 (The puresat algorithm)"
Previous message: Zaher S Andraus: "Can't run check_invariant -A4 (The puresat algorithm)"
In reply to: Zaher S Andraus: "Can't run check_invariant -A4 (The puresat algorithm)"
Next in thread: Zaher S Andraus: "Re: Can't run check_invariant -A4 (The puresat algorithm)"
Reply: Zaher S Andraus: "Re: Can't run check_invariant -A4 (The puresat algorithm)"
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 Mar 30 2007 - 16:18:39 MDT