Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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