z3: strip (exit)/(get-model) before appending the tactic

Many SMT-LIB files end with `(check-sat) (exit)`. The preprocessing stripped
only `(check-sat)` and appended `(apply <tactic>)` at the end, so a leftover
`(exit)` made z3 quit before the tactic ran -> empty output -> silent fallback
to the unsimplified file. On the real SMT-COMP QF_FP set this made --simplify a
no-op (handled 3/151); with the fix it handles 125/151 (the rest declare a
RoundingMode variable, which the evaluator doesn't model).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Author: shaobo-he

src/z3.rs

@@ -181,11 +181,18 @@ fn apply_z3_tactic(path: &str, tactic: &str, tag: &str) -> std::io::Result<std::
         .filter(|e| matches!(e.head_sym(), Some("declare-const") | Some("declare-fun")))
         .collect();
 
+    // Strip the trailing solver commands and append the tactic application.
+    // We must remove `(exit)` (and `(get-model)` etc.) too, not just
+    // `(check-sat)`: many SMT-LIB files end with `(check-sat) (exit)`, and a
+    // leftover `(exit)` makes z3 quit *before* reaching the appended tactic
+    // (producing empty output and a silent fallback to the unsimplified file).
+    let stripped = raw
+        .replace("(check-sat)", "")
+        .replace("(exit)", "")
+        .replace("(get-model)", "")
+        .replace("(get-unsat-core)", "");
     let tactic_file = temp_path(&format!("{tag}-in"));
-    std::fs::write(
-        &tactic_file,
-        format!("{}\n(apply {tactic})\n", raw.replace("(check-sat)", "")),
-    )?;
+    std::fs::write(&tactic_file, format!("{stripped}\n(apply {tactic})\n"))?;
     // If z3 is unavailable, transparently fall back to the original file.
     let output = match run_z3(&tactic_file) {
         Ok(o) => o,