CVC4 1.7 hates predefined symbols
function exp int: int goal G: true
$ bin/why3 prove -P CVC4,1.7 foo.mlw foo.mlw Top G: HighFailure (0.02s) Prover exit status: killed by signal 11 Prover output: (error "Parse Error: /tmp/why_72ac78_foo-T-G.smt2:9.16: Symbol `exp' is shadowing a theory function symbol (declare-fun exp (Int) Int) ^ ") CVC4 suffered a segfault. Offending address is 0x8 Looks like a NULL pointer was dereferenced.
exp case is fixed by 290333ce, but there might be other cases.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information