Invariant Synthesis - #120

Draft

maditaP wants to merge 11 commits into

moves-rwth:mainfrom

maditaP:rebased/invariant-synthesis

Commits on Jun 17, 2026

z3: add z3.rs submodule and switch Cargo to local path
maditaP
committed
a54fd38
ast/smt: add signed integer literals
maditaP
committed
fd87c5b
ast: add range syntax
maditaP
committed
9ebe390
ast: add syn function declarations
maditaP
committed
881d2f7
ast: RemoveCastsVisitor strips nested casts
maditaP
committed
099b78c
intrinsic: add nonneg_cast
maditaP
committed
4bd4321
smt: translate Iverson brackets to numeric types
maditaP
committed
299e71f
opt: add NeutralsRemover optimizer
maditaP
committed
a0fe56b
synthesis: introduce template-based CEGIS invariant synthesis
maditaP
committed
99bf049
z3rro: fix model evaluation for large and negative values
maditaP
committed
cf18e5c
tests: add synthesis benchmark test suite
maditaP
committed
e1b84a4