Issues · Why3 / why3 · GitLab

Isabelle/HOL back-end does not support Why3 arrays

#655 · created May 30, 2022 by MARCHE Claude component: drivers
- 0
updated May 30, 2022
Pattern matching with record leads to a crash for CVC4 & Z3

#644 · created May 05, 2022 by Guillaume Cluzel To be discussed component: drivers
- 4
updated May 23, 2022
z3 driver should not unfold definitions

#611 · created Feb 04, 2022 by MARCHE Claude ProofInUse/TrustInSoft To be discussed component: drivers
- 1
updated May 20, 2022
wish: provide monomorphic, clonable modules for references and arrays

#567 · created Mar 31, 2021 by MARCHE Claude To be discussed component: drivers component: theories component: transformations
- 14
updated Mar 22, 2022
Add floating-point support by Alt-Ergo FPA and mathsat

#438 · created Jan 28, 2020 by MARCHE Claude component: drivers
- 9
updated Mar 22, 2022
SMT support for solvers which do not support quantifiers

#437 · created Jan 28, 2020 by MARCHE Claude component: drivers
- 1
- 0
updated Mar 22, 2022
overly generic logics declaration causes slowdown of cvc4 proof

#362 · created Jul 04, 2019 by Johannes Kanig To be discussed component: drivers
- 7
updated Oct 28, 2020
CVC4 for smtlib 2.6

#272 · created Feb 11, 2019 by DAILLER Sylvain component: drivers
- 3
updated Mar 22, 2022
Division and comparison in SMT and Alt-ergo

#242 · created Nov 26, 2018 by François Bobot component: drivers
- 1
updated Feb 11, 2021