[PARKED] Use uninterpreted functions for 2-phase solving approach - #996

Closed

gustavo-grieco wants to merge 136 commits into

mainfrom

poc-div-encoding

Commits on Feb 17, 2026

proof of concept of of div-encoding

gustavo-grieco
authored and
msooseth
committed
038d31a
axioms

gustavo-grieco
authored and
msooseth
committed
536e063
avoid unsoundness

gustavo-grieco
authored and
msooseth
committed
0513779
fixes and tests

gustavo-grieco
authored and
msooseth
committed
b687ca8
fixes

gustavo-grieco
authored and
msooseth
committed
113a25a
Update src/EVM/SMT/DivEncoding.hs
msooseth
committed
f3e103e
fixes

gustavo-grieco
authored and
msooseth
committed
3d995ed
Remove warning
msooseth
committed
21cd753
Cleanup
msooseth
committed
e73af5a
Cleanup
msooseth
committed
45b71c5
Rename, lineup
msooseth
committed
8716a51
Fix code repetition
msooseth
committed
f4d7fdf
Cleanup
msooseth
committed
e60173a
Waaay cleaner setup
msooseth
committed
df399c6
Update cabal
msooseth
committed
81d2690
Less obvious comments
msooseth
committed
e03cd05
Cleanup
msooseth
committed
1c48980
Cleanup
msooseth
committed
1dad96c
Cleaner
msooseth
committed
c3112cd
Cleanup
msooseth
committed
40bd88c
Cleanup
msooseth
committed
d9c5089
Cleanup
msooseth
committed
d1f5333
Cleanup
msooseth
committed
d24dfdd
Cleanup
msooseth
committed
7554795
Update
msooseth
committed
ce537e1
Cleanup
msooseth
committed
d20beeb
Fixing
msooseth
committed
b07ee28
assertProps is now abst+axioms+refine
msooseth
committed
de82732
Update
msooseth
committed
3ad2715
Proper 2-phase
msooseth
committed
6816fc9
Cleanup
msooseth
committed
1f654ec
OK, now doing assertProps on its own as well
msooseth
committed
b20e92d
Better comments
msooseth
committed
51e93d1
No more exprToSMT
msooseth
committed
e65f984
Fixing testing
msooseth
committed
6a55da8
Cleanup
msooseth
committed
c7e543f
Cleanup
msooseth
committed
a9a86c8
Fixing
msooseth
committed
ae8fb7f
Cleanup
msooseth
committed
0e6403b
Less code
msooseth
committed
38eec42
I think this is better
msooseth
committed
8901ba6
Fixing
msooseth
committed
327fe28
Update
msooseth
committed
560dce3
Cleanup
msooseth
committed
36b9b05
Cleanup
msooseth
committed
fd796b0
Flush output buffer via traceM
msooseth
committed
4ef42ae
Making more progress
msooseth
committed
d6ed757
Rename
msooseth
committed
ce1bd7a
Cleaner code
msooseth
committed
2d72720
OK, let's try this?
msooseth
committed
0e25ff9
Remove nonsense comment
msooseth
committed
de03abf
Moving code lower
msooseth
committed
7a42090
Cleanup
msooseth
committed
96e0980
None of this 1-K stuff, also correct Cex handing on 3rd phase
msooseth
committed
cb15623
Maybe cleaner
msooseth
committed
3cb47e0
Rename
msooseth
committed
a2bf7f1
Better naming
msooseth
committed
52edee6
More cleanup
msooseth
committed
cd5333f
More cleanup
msooseth
committed
d9ac366
Cleanup
msooseth
committed
0b0d161
Better printing
msooseth
committed
e0abb57
Cleaner
msooseth
committed
bf5e111
Cleanup
msooseth
committed
c38dcbf
Cleaning up comments
msooseth
committed
ca534eb
Cleaner
msooseth
committed
ec81d15
Fix spacing
msooseth
committed
bb54f86
Even cleaner
msooseth
committed
4c82008
Update
msooseth
committed
15038e8
Cleanup
msooseth
committed
29acc17
Moving functions, sorry!
msooseth
committed
c68cd6e
Cleanupo
msooseth
committed
5fbf561
Better naming
msooseth
committed
114b4ce
Better naming
msooseth
committed
1f350e5
Adding div/mod bounds
msooseth
committed
e73cfc6
More
msooseth
committed
7b54eb4
Cleanup
msooseth
committed
3b180b9
Better comments
msooseth
committed
73c1d9a
Update
msooseth
committed
7c093e4
Cleanup
msooseth
committed
7c88e62
Cleanup
msooseth
committed
d057c91
Cleanup
msooseth
committed
6072b47
Cleanup
msooseth
committed
85dc0b4
Fixing
msooseth
committed
c1ac1ce
Update
msooseth
committed
7447f0d
Cleanup
msooseth
committed
66f14aa
Now without divmod
msooseth
committed
4d775f3
Even less
msooseth
committed
b40f875
Cleanup
msooseth
committed
94d98a8
Cleanup
msooseth
committed
2d4d344
Cleanup
msooseth
committed
9476412
Update
msooseth
committed
d0ef06b
Better
msooseth
committed
b2b8b4f
Better printing
msooseth
committed
359f5dc
Move
msooseth
committed
4de3a17
Update
msooseth
committed
d5d2659
Update tests
msooseth
committed
05198eb
Cleanup
msooseth
committed
0002c69
Adding tests
msooseth
committed
d7bdb55
Cleanup
msooseth
committed
36221ec
Fix dumping
msooseth
committed
0aebdfb
Fix dumping
msooseth
committed
936280b

Commits on Feb 18, 2026

Better
msooseth
committed
8bef599
Update
msooseth
committed
706952e
Better
msooseth
committed
a0baa04
Update
msooseth
committed
ba22aac
Update naming
msooseth
committed
81c766a
Cleanup
msooseth
committed
48bc777
Cleanup
msooseth
committed
2426e88
Fixing warning
msooseth
committed
bf156b3
Rename
msooseth
committed
2763078
Fix name of file
msooseth
committed
49296dd
Fixing cabal
msooseth
committed
503d110
No need for this
msooseth
committed
251aef0
Fixing up cli test
msooseth
committed
c95d5f8
No need for these printings
msooseth
committed
0fb590c
Fixing this test
msooseth
committed
a4ef47e
Rename
msooseth
committed
92df580
Fixing val
msooseth
committed
13ad8de
Named correctly
msooseth
committed
898fca9
Fixing naming
msooseth
committed
1d63c63
Renaming
msooseth
committed
4e06446
Update name
msooseth
committed
f3213dd
Update
msooseth
committed
f087d98
Adding test, ifxing import, fixing printing
msooseth
committed
0ab6fb4
Adding the tests
msooseth
committed
1304d32
Cleaner
msooseth
committed
fcb8645
Cleanup
msooseth
committed
1838ea7

Commits on Apr 6, 2026

import fix
gustavo-grieco
committed
cf21972
Merge remote-tracking branch 'origin/main' into poc-div-encoding
gustavo-grieco
committed
5d5cfe0
more fixes
gustavo-grieco
committed
7aaefd0
ignore math-mint-fail test
gustavo-grieco
committed
4b18b03

Commits on Apr 30, 2026

Merge branch 'main' into poc-div-encoding
gustavo-grieco
authored
7f991f6

Commits on Jun 17, 2026