Simon Cruanes af8ab338e6 feat(smt): add a registry to share values between theories		2022-01-11 14:00:04 -05:00
..
arith	fix theory combination for LRA	2022-01-11 14:00:04 -05:00
base	fix LIA->LRA cast operation	2022-01-11 14:00:04 -05:00
base-solver	fix theory combination for LRA	2022-01-11 14:00:04 -05:00
bin-lib
cc	fix(CC): bug introduced by sharing mutable lazy state	2022-01-10 12:11:32 -05:00
checker
core	feat(smt): add a registry to share values between theories	2022-01-11 14:00:04 -05:00
drup
lit
lra	fix theory combination for LRA	2022-01-11 14:00:04 -05:00
main	use TEF in sudoku; improve a bit its ergonomics	2021-12-07 21:29:51 -05:00
memtrace
mini-cc
proof-trace	feat: proper proof production for theory merges in CC	2021-12-29 15:56:54 -05:00
proof-trace-dump
quip	clause-less steps in proofs	2022-01-03 22:59:43 -05:00
sat	fix(sat): use a set of delayed actions	2022-01-11 14:00:03 -05:00
sigs
smt-solver	feat(smt): add a registry to share values between theories	2022-01-11 14:00:04 -05:00
smtlib	fix LIA->LRA cast operation	2022-01-11 14:00:04 -05:00
tef	use TEF in sudoku; improve a bit its ergonomics	2021-12-07 21:29:51 -05:00
tests
th-bool-dyn
th-bool-static	feat: proper proof production for theory merges in CC	2021-12-29 15:56:54 -05:00
th-cstor
th-data	feat: proper proof production for theory merges in CC	2021-12-29 15:56:54 -05:00
tools
util	feat(util): add backtrackable ref	2021-12-07 14:08:06 -05:00
zarith	feat: add Q.is_int	2022-01-11 14:00:03 -05:00
dune	build flags	2021-11-29 10:33:56 -05:00