--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on August 2014 ---
Hello, I have a problem to get jessie3 on frama-c neon working (see below). It claims that it could not find z3 solver (but its installed, removing prover z3 from ~/.why3.conf does also not help. Any ideas whats wrong in my setup? My setup: ====== - Ubuntu 14.04 - Z3 [version 4.3.1 - 64 bit] (manuell kompiliert) - alt-ergo 0.95.2-1build1 - coq 8.4pl3dfsg-1 - coq-theories 8.4pl3dfsg-1 - Why3 platform, version 0.83 (build date: Mon Aug 11 18:23:24 CEST 2014) (manuell kompiliert) - /usr/local/bin/frama-c --version Version: Neon-20140301 Compilation date: Sat Aug 9 14:16:12 CEST 2014 Share path: /usr/local/share/frama-c (may be overridden with FRAMAC_SHARE variable) Library path: /usr/local/lib/frama-c (may be overridden with FRAMAC_LIB variable) Plug-in paths: /usr/local/lib/frama-c/plugins (may be overridden with FRAMAC_PLUGIN variable) why3config --detect Found prover Alt-Ergo version 0.95.2, Ok. Found prover Z3 version 4.3.1, Ok. Found prover Coq version 8.4pl3, Ok. 3 provers detected and 0 provers detected with unsupported version == Found /usr/local/lib/why3/plugins/dimacs.cmxs == == Found /usr/local/lib/why3/plugins/hypothesis_selection.cmxs == == Found /usr/local/lib/why3/plugins/tptp.cmxs == == Found /usr/local/lib/why3/plugins/genequlin.cmxs == Save config to /home/crissi/.why3.conf Program ====== void main() { int N = 10; int s = 0; int k = 0; /*@ requires N >= 0 && s == 0 && k == 0 ; @ ensures k == N * N ; */ while (k<N) { // @ ensures s >= 0 ; s = s+2*k+1; // @ ensures k >= 0; k = k+1; } } Log ==== /usr/local/bin/frama-c -jessie3 -debug 1 -jessie3-verbose 3 fv_aufgabe1.c [jessie3] Loading Why3 configuration... [jessie3] Why3 environment loaded. [jessie3] Loading Why3 theories... [jessie3] Loading Why3 modules... [jessie3] Looking up module mach.int.Int32 [jessie3] Looking up module mach.int.Int64 [kernel] preprocessing with "gcc -C -E -I. fv_aufgabe1.c" [jessie3] Loading prover drivers... [jessie3] failure: Prover Z3,3.2 not installed or not configured [jessie3] failure: Exception raised when loading prover drivers: anomaly: Log.AbortFatal("jessie3") [kernel] Current source was: fv_aufgabe1.c:1 [kernel] The full backtrace is: [kernel] Raised at file "src/kernel/log.ml", line 524, characters 30-31 [kernel] Called from file "src/kernel/log.ml", line 518, characters 9-16 [kernel] Re-raised at file "src/kernel/log.ml", line 521, characters 15-16 [kernel] Called from file "register.ml", line 71, characters 6-113 [kernel] Called from file "queue.ml", line 134, characters 6-20 [kernel] Called from file "src/kernel/boot.ml", line 37, characters 4-20 [kernel] Called from file "src/kernel/cmdline.ml", line 735, characters 2-9 [kernel] Called from file "src/kernel/cmdline.ml", line 214, characters 4-8 [kernel] [kernel] Plug-in jessie3 aborted: internal error. [kernel] Please report as 'crash' at http://bts.frama-c.com/. [kernel] Your Frama-C version is Neon-20140301. [kernel] Note that a version and a backtrace alone often do not contain enough [kernel] information to understand the bug. Guidelines for reporting bugs are at: [kernel] http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines With best regards Christoph