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

[Frama-c-discuss] (no subject)



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