[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Bug#906001: why3: needs porting to cvc4 version 1.6



Package: why3
Version: 1.0.0-1
Forwarded: https://gitlab.inria.fr/why3/why3/issues/164

why3 does not yet support version 1.6 of cvc4:

$ why3 config --detect-provers
[..]
warning: Prover CVC4 version 1.6 is not known to be supported.

$ why3 prove -P 'CVC4' minimum.mlw
minimum.mlw Minimum VC minimum: HighFailure (0.00s)
Prover exit status: exited with status 1
Prover output:
(error "Parse Error: /tmp/why_e2c49a_minimum-T-VC_minimum.smt2:8.24: Too many datatypes defined in this block.

  (declare-datatypes () ((tuple0 (Tuple0))))
                          ^
")

-Ralf.


Reply to: