search

CatarinaGamboa / liquidjava

32 stars 1 forks source link

Can Z3 new Simplifier help error messages? #22

Open alcides opened 1 year ago

alcides commented 1 year ago

Z3 Nightly now has a Simplifier API available in Java: https://github.com/Z3Prover/z3/commit/4143c542571948368a6a36334a21392ed50ddb3f https://github.com/Z3Prover/z3/releases/tag/Nightly

Can this be used to improve error messages?

alcides commented 4 hours ago

Rethinking this, I am not sure it can be used directly. I am exploring simplification in Aeon, and we are doing simplification by hand, which seems more useful for tracing the origins.