dolmen
forked from gbury/dolmen
Star 1
Fork 0
Watch

Version history of src/loop/typer.ml

August 2026

Guillaume Bury
Add support for SMT-LIB's :global-declarations options (#269)
committed
Guillaume Bury
Implement 'dumb' polymophism for SMT-LIB + various HO fixes (#268)
committed

July 2026

Guillaume Bury
Split HO into a separate builtin theory for typechecking (#267)
committed
Guillaume Bury
Add Integer exponentiation (#259)
committed

February 2026

Guillaume Bury
Fixes for implicit type vars and datatype decls in smt-lib
committed

August 2025

Guillaume Bury
Prevent overlapping of parameters in def-fun in SMT-LIB (#247)
committed
Guillaume Bury
Reject overlapping parallel bindings (#246)
committed
Guillaume Bury
Smtlib Printer (#211)
committed
Guillaume Bury
Reject SMT-LIB2 distinct applications to less than 2 arguments (#243)
committed

May 2025

Guillaume Bury
Fixes for model validation in smt2.7
committed

April 2025

Guillaume Bury
Support for SMT-LIB 2.7 (#235)
committed

March 2025

Basile Clément
feat: Add support for user-defined builtins with Dune plugins (#214)
committed
Basile Clément
feat: Support more Alt-Ergo primitives (#220)
committed

March 2024

Guillaume Bury
Add warning for unknown attribute (#207)
committed
Guillaume Bury
Add typing extensions, and the bvconv extension (#208)
committed

November 2023

Guillaume Bury
Add proper support for `:named` smtlib annotations (#199)
committed

October 2023

Guillaume Bury
More information for reserved id, and adjusted errors
committed
Guillaume Bury
Replace `Plain` with `Other` and assorted fixes
committed

September 2023

Guillaume Bury
Refine some arithmetic error/warning messages (#184)
committed

July 2023

Guillaume Bury
More checks on bitvector size for extract
committed
Guillaume Bury
Enforce constraints on bitvectors indexes
committed

June 2023

Guillaume Bury
Propagate annotations to typed statements
committed
Basile Clément
Add support for prelude files
committed
Pierrot
Support check_sat statement for Alt-Ergo language (#140)
committed
Hichem R. A
Support more Bit-Vector primitives in Alt-Ergo's native language (#136)
committed
Guillaume Bury
Fix reason for reserved builtins (#155)
committed
Guillaume Bury
Implement best mode for model verification (#154)
committed
Guillaume Bury
Add printing of type definitions in debug output (#157)
committed
Guillaume Bury
Some more printing (#142)
committed

May 2023

Guillaume Bury
Model fixes (#151)
committed

March 2023

Guillaume Bury
Add some doc (plus some small refactorings)
committed

January 2023

Guillaume Bury
Multliple fixes for recursive definitions (#123)
committed

December 2022

Guillaume Bury
Fix windows build and tests (#117)
committed

October 2022

Hichem R. A
Expose Term Consts (#112)
committed
Guillaume Bury
Add to state keys the name of the module responsible for their init
committed
Guillaume Bury
Group state keys by module with an init function
committed

September 2022

Guillaume Bury
Add dedictaed typing errors for sexprs
committed

July 2022

Guillaume Bury
Rename Check->Response for smtlib2 response files
committed
Guillaume Bury
Add option to force an smtlib2 logic
committed

June 2022

Guillaume Bury
Better handling of corner cases in models + adjusted err/warn messages
committed
Guillaume Bury
Cleanup handling of definitions
committed
Guillaume Bury
WIP
committed
Guillaume Bury
Support division by zero in models (when specified by the model)
committed
Guillaume Bury
Add support for ADTS in model verification
committed
Guillaume Bury
Change state to hmap to simplify deps between modules
committed
Guillaume Bury
More error messages + take into account defs in original problem
committed
Guillaume Bury
Working first prototype
committed
Guillaume Bury
WIP
committed
Guillaume Bury
WIP
committed
Guillaume Bury
Somewhat working
committed