From b6502ed917c9c8ecc6670173180164a876dc9536 Mon Sep 17 00:00:00 2001
From: Karlheinz Friedberger <kfriedberger@gmail.com>
Date: Mon, 12 Jun 2023 20:30:32 +0200
Subject: [PATCH] Z3: update list of known interrupts for exceptions.

---
 src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java
index 9b8c248c8f..dc5c5bc62a 100644
--- 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