--- layout: fc_discuss_archives title: Message 76 from Frama-C-discuss on June 2009 ---
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 -------------- next part -------------- A non-text attachment was scrubbed... Name: not available Type: application/ms-tnef Size: 3119 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090623/1ce05e7e/attachment-0001.bin