--- layout: fc_discuss_archives title: Message 114 from Frama-C-discuss on September 2013 ---
Hi all, I have installed Z3 version 4.3.1 and why3config --detect Found prover Alt-Ergo version 0.94 (it is an old version that is less tested than the current one). Found prover Z3 version 4.3.1, Ok. Found prover Coq version 8.3pl4, Ok. Found prover PVS version 6.0, Ok. 4 provers detected and 0 provers detected with unsupported version == Found /usr/local/lib/why3/plugins/dimacs.cmxs == == Found /usr/local/lib/why3/plugins/tptp.cmxs == == Found /usr/local/lib/why3/plugins/hypothesis_selection.cmxs == == Found /usr/local/lib/why3/plugins/genequlin.cmxs == Perhaps I missed something important in configuration of frama-c and why3 when I got the following error. <mymachine>:~/formal/frama-c-Fluorine-20130601/tests/swap$ frama-c -jessie3 swap.c swap2.c [kernel] preprocessing with "gcc -C -E -I. swap.c" [kernel] preprocessing with "gcc -C -E -I. swap2.c" [jessie3] failure: Prover Z3,3.2 not installed or not configured [kernel] Current source was: swap.c:1 The full backtrace is: Raised at file "src/kernel/log.ml", line 523, characters 30-31 Called from file "src/kernel/log.ml", line 517, characters 9-16 Re-raised at file "src/kernel/log.ml", line 520, characters 15-16 Called from file "register.ml", line 43, characters 8-80 Called from file "list.ml", line 74, characters 24-34 Called from file "register.ml", line 59, characters 4-209 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 37, characters 4-20 Called from file "src/kernel/cmdline.ml", line 732, characters 2-9 Called from file "src/kernel/cmdline.ml", line 212, characters 4-8 Plug-in jessie3 aborted: internal error. Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Fluorine-20130601. Note that a version and a backtrace alone often do not contain enough information to understand the bug. Guidelines for reporting bugs are at: http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines Does nyone can advice ? Thanks in advance -- Dragan Stosic Senior developer at IBM phone: 085-773-1050 e-mail: dragan.stosic at gmail.com e-mail:DRAGANST at ie.ibm.com IBM Technology Campus Damastown Industrial Estate Mulhuddart Dublin 15 Ireland -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130918/ef622cc7/attachment.html>