--- layout: fc_discuss_archives title: Message 78 from Frama-C-discuss on June 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] (no subject)



sorry, I forgot to tell:
it's yices 1.0.15 and cvc3 1.5 

Kerstin



----------

This has to do with versions of Yices and CVC3, what are they ?

Kerstin Hartig wrote:
> Hi,
> 
> $ why-cpulimit 10 cvc3 -lang smt < /cygdrive/c/Dokumente\ und\ Einstellungen/Ad
> ministrator/Lokale\ Einstellungen/Temp/gwhy81903f_why.smt
> --> nothing happens
> 
> why-cpulimit 10 yices -pc 0 smt < /cygdrive/c/Dokumente\ und\ Einstellungen/Administrator/Lokale\ Einstellungen/Temp/gwhy70ef43_why.smt
> --> Error at 1: Unexpected token '(null)', '(' expected.
> 
> the first lines of gwhy70ef43_why.smt:
> 
> (benchmark gwhy70ef43
>   :status unknown
>   :logic AUFLIA
>   :extrasorts (c_Boolean)
>   :extrafuns ((c_Boolean_true c_Boolean))
>   :extrafuns ((c_Boolean_false c_Boolean))
>   :assumption
>                   (forall (?bcd c_Boolean) (or (= ?bcd c_Boolean_true)
>                                             (= ?bcd c_Boolean_false)))
>   :assumption
>                   (not
>                       (= c_Boolean_true  c_Boolean_false))
>   :extrasorts (Unit)
>   :extrafuns ((div_int Int Int Int))
>   :extrafuns ((modulo Int Int Int))
> :extrasorts (c_unsorted)
> :extrasorts (c_sorted)
> :extrasorts (c_type)
> ;;;; Why logic c_int
> :extrafuns ((c_int  c_type))
> 
> ;;;; Why logic c_bool
> :extrafuns ((c_bool  c_type))
> 
> ;;;; Why logic c_real
> :extrafuns ((c_real  c_type))
> 
> ;;;; Why logic c_unit
> :extrafuns ((c_unit  c_type))
> 
> ;;;; Why logic c_sort
> :extrafuns ((c_sort c_type c_unsorted c_sorted))
> 
> ;;;; Why logic int2u
> :extrafuns ((int2u Int c_unsorted))
> 
> ;;;; Why logic bool2u
> :extrafuns ((bool2u c_Boolean c_unsorted))
> 
> ....
> 
> thanx,
> 
> Kerstin
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |







_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/ms-tnef
Size: 3739 bytes
Desc: not available
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090623/0cb9dc42/attachment.bin