Retrieving Unknown SMT Formulas via Structural Mutations
summary
Claim: unknown SMT formulas often become decidable by simple syntactic edits and running the same solver on those variants in parallel. Method mutates formulas by structural mutations (removing assertions, replacing subterms, under/over-approximations) and treats any informative solver reply as proof for the original via one-sided guarantees. Implemented as a lightweight, solver-agnostic parallel driver tested on SMT-LIB with Z3 and CVC4 showing multiple previously unknown cases resolved and usable unsat cores.
AI-written summary · about