--- layout: fc_discuss_archives title: Message 78 from Frama-C-discuss on June 2009 ---
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