Z3: update list of known interrupts for exceptions.

sosy-lab · Jun 12, 2023 · b6502ed · b6502ed
1 parent f611214
commit b6502ed
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java
@@ -98,6 +98,8 @@ class Z3FormulaCreator extends FormulaCreator<Long, Long, Long, Long> {
   private static final ImmutableSet<String> Z3_INTERRUPT_ERRORS =
       ImmutableSet.of(
           "canceled", // Z3::src/util/common_msgs.cpp
+          "push canceled", // src/smt/smt_context.cpp
+          "interrupted from keyboard", // Z3: src/solver/check_sat_result.cpp
           "Proof error!",
           "interrupted", // Z3::src/solver/check_sat_result.cpp
           "maximization suspended" // Z3::src/opt/opt_solver.cpp