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.
The exp
case is fixed by 290333ce, but there might be other cases.