Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. updated SMT certificates and added one test
  2. updated NEWS
  3. properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
Changeset 66740:ece9435ca78e by blanchet:
updated SMT certificates and added one test
The file was modified src/HOL/SMT_Examples/Boogie.thy (diff)
The file was modified src/HOL/SMT_Examples/Boogie_Dijkstra.certs (diff)
The file was modified src/HOL/SMT_Examples/SMT_Examples.certs (diff)
The file was modified src/HOL/SMT_Examples/SMT_Examples.thy (diff)
Changeset 66739:1e5c7599aa5b by blanchet:
updated NEWS
The file was modified NEWS (diff)
Changeset 66738:793e7a9c30c5 by blanchet:
properly take quantifiers into account (cf. my Ph.D. thesis, Section 6.4.1) and offer three modes of completeness (for experiments mostly)
The file was modified src/HOL/SMT_Examples/SMT_Tests.thy (diff)
The file was modified src/HOL/Tools/SMT/smt_config.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_translate.ML (diff)