Page MenuHomeIsabelle/Phabricator

mathias.fleury (Mathias Fleury)
User

Projects

User Details

User Since
Oct 29 2020, 2:12 PM (27 w, 5 d)

Recent Activity

Mar 17 2021

mathias.fleury added a comment to T29: Update component for Z3.

Basically currently the proof format of Z3 has bugs that we cannot solve on the Isabelle side (https://github.com/Z3Prover/z3/issues/5073). Fixing those requires either internal Z3 knowledge or time from a Z3 developer.

Mar 17 2021, 6:28 PM · provers

Jan 8 2021

mathias.fleury committed rISABELLE6520d59fbdd7: ignore error messages produced by CVC4 when generating BV.
ignore error messages produced by CVC4 when generating BV
Jan 8 2021, 8:40 PM

Dec 15 2020

mathias.fleury committed rISABELLEf9424ceea3c3: don't generate not-fully-defined bit-vector constants in SMT problems.
don't generate not-fully-defined bit-vector constants in SMT problems
Dec 15 2020, 4:53 PM
mathias.fleury committed rISABELLE6a26a955308e: improve and activate compression for veriT proof reconstruction.
improve and activate compression for veriT proof reconstruction
Dec 15 2020, 7:00 AM

Oct 31 2020

mathias.fleury closed T25: Update component for veriT as Resolved.

The veriT version is sufficient for the next release.

Oct 31 2020, 7:18 AM · provers, isabelle-release