User Details
User Details
- User Since
- Oct 29 2020, 2:12 PM (182 w, 1 d)
Feb 5 2024
Feb 5 2024
fix reconstruction of Alethe's and_pos rule
Aug 1 2023
Aug 1 2023
remove debug printing
Jul 26 2023
Jul 26 2023
support for let in Alethe name bindings;
Jun 19 2023
Jun 19 2023
mathias.fleury committed rISABELLEea7a3cc64df5: early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals;.
early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals;
Aug 29 2022
Aug 29 2022
replace smt_oracle by proper veriT reconstruction
Aug 22 2022
Aug 22 2022
mathias.fleury committed rISABELLE1e2a9d2251b0: remove duplicate parsing for alethe; fix skolemization;.
remove duplicate parsing for alethe; fix skolemization;
Jun 25 2022
Jun 25 2022
missing recursive let-expansion in SMT translation
Jun 14 2022
Jun 14 2022
mathias.fleury committed rISABELLEb6239ed66b94: fix veriT reconstruction for and_pos and lambda-lifting.
fix veriT reconstruction for and_pos and lambda-lifting
Mar 22 2022
Mar 22 2022
mathias.fleury committed rISABELLEda591621d6ae: split veriT reconstruction into Lethe and veriT part.
split veriT reconstruction into Lethe and veriT part
Mar 11 2022
Mar 11 2022
mathias.fleury committed rISABELLE73650a19591d: fix handling of lambdas in reconstruction of eq_congruent.
fix handling of lambdas in reconstruction of eq_congruent
Nov 26 2021
Nov 26 2021
generate problems with correct logic for veriT
Nov 4 2021
Nov 4 2021
proper support of verit's return code for timeout
Oct 1 2021
Oct 1 2021
update syntax for verit
Mar 17 2021
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.
Jan 8 2021
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
Dec 15 2020
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
mathias.fleury committed rISABELLE6a26a955308e: improve and activate compression for veriT proof reconstruction.
improve and activate compression for veriT proof reconstruction
Oct 31 2020
Oct 31 2020
The veriT version is sufficient for the next release.