mirror of
https://github.com/Z3Prover/z3
synced 2025-04-17 22:35:35 +00:00
- add outline of trim routine - streamline how proof terms are checked and how residue units are extracted. |
||
---|---|---|
.. | ||
arith_rewriter_params.pyg | ||
array_rewriter_params.pyg | ||
bit_blaster_params.h | ||
bool_rewriter_params.pyg | ||
bv_rewriter_params.pyg | ||
CMakeLists.txt | ||
context_params.cpp | ||
context_params.h | ||
fpa2bv_rewriter_params.pyg | ||
fpa_rewriter_params.pyg | ||
pattern_inference_params.cpp | ||
pattern_inference_params.h | ||
pattern_inference_params_helper.pyg | ||
poly_rewriter_params.pyg | ||
rewriter_params.pyg | ||
seq_rewriter_params.pyg | ||
solver_params.pyg |