Raghav/weakest precondition#41

Merged

raghav198 merged 60 commits into

mainfrom

raghav/weakest-precondition

Jul 10, 2026

Commits on May 26, 2026

Added cvc5 dependency
Raghav Malik
committed
Test run of cvc5 expression building
Raghav Malik
committed

Commits on May 27, 2026

lmao
Raghav Malik
committed
First pass of WP calculator is done, but memory issues
Raghav Malik
committed

Commits on May 28, 2026

oops
Raghav Malik
committed
ugh
Raghav Malik
committed
Trying without StringMap
Raghav Malik
committed
Fixed stupid lifetimes issue
Raghav Malik
committed
fixed memory errors, and (a -> (b -> c)) to (a && b) -> c
Raghav Malik
committed
Reducing mod p now, still need to fix field inference
Raghav Malik
committed
Refactor with TermBuilder
Raghav Malik
committed
Bump LLZK, clean up field detection
Raghav Malik
committed

Commits on May 29, 2026

update comment
Raghav Malik
committed
Merge remote-tracking branch 'origin' into raghav/weakest-precondition
Raghav Malik
committed

Commits on Jun 1, 2026

Updated tests for optimized SMT encoding
Raghav Malik
committed
Bump LLZK
Raghav Malik
committed
Don't spuriously require field
Raghav Malik
committed
Rename
Raghav Malik
committed

Commits on Jun 2, 2026

Properly handle WP for arrays
Raghav Malik
committed
Made array flattening optional
Raghav Malik
committed
marked regression
Raghav Malik
committed
Emitting extra declarations, added some TODOs
Raghav Malik
committed

Commits on Jun 4, 2026

Array equality works after adding bounds
Raghav Malik
committed
Some refactoring, whatever
Raghav Malik
committed
Emit extra [0, p-1] bounds
Raghav Malik
committed

Commits on Jun 8, 2026

Add readwrite array test
Raghav Malik
committed
Really stupid handling of subcomponents, not emitting extra uninterpreted func/sort decls yet
Raghav Malik
committed
Always doing write-once semantics for signal arrays, still need to make this a flag and don't mod array selects
Raghav Malik
committed

Commits on Jun 11, 2026

Some better subcomponent support in WP
Raghav Malik
committed

Commits on Jun 12, 2026

Fixed testcases
Raghav Malik
committed
syntax error in test I guess
Raghav Malik
committed
Subcomponent store

raghav198
and
Raghav Malik
authored

Commits on Jun 24, 2026

Loop invariants (#43)

raghav198
and
Raghav Malik
authored

Commits on Jun 25, 2026

Raghav/public release (#50)

raghav198
and
Raghav Malik
authored
Revert "Raghav/public release (#50)"
Raghav Malik
committed

Commits on Jun 30, 2026

Raghav/public release (#55)

raghav198
and
Raghav Malik
authored
Correctly read from a subcomponent member
Raghav Malik
committed

Commits on Jul 1, 2026

Correctly read from a subcomponent member
Raghav Malik
committed
Implemented solver portfolio
Raghav Malik
committed

Commits on Jul 2, 2026

bn128
Raghav Malik
committed
git module
Raghav Malik
committed
Fixed portfolio issues, added benchmark importing
Raghav Malik
committed
Remove hardcoded benchmarks
Raghav Malik
committed

Commits on Jul 7, 2026

Remove unused file
Raghav Malik
committed
Documentation
Raghav Malik
committed
Veridise Inc -> Project LLZK
Raghav Malik
committed
Comments
Raghav Malik
committed
Comments, got rid of missing file from cmake
Raghav Malik
committed
Code review comments
Raghav Malik
committed
Veridise Inc -> Project LLZK
Raghav Malik
committed
Build instructions clearer
Raghav Malik
committed
Reword
Raghav Malik
committed
Reword
Raghav Malik
committed
Veridise Inc -> Project LLZK
Raghav Malik
committed
Updated report syntax
Raghav Malik
committed
Updated report syntax
Raghav Malik
committed

Commits on Jul 8, 2026

Bump LLZK
Raghav Malik
committed
default to release build
Raghav Malik
committed
Code review comments
Raghav Malik
committed

Commits on Jul 10, 2026

Code review comments
Raghav Malik
committed