diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index a44a7659b..b5d64d345 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2253,7 +2253,9 @@ public: } lbool lbl = make_feasible(); - + if (m.canceled()) + return; + switch(lbl) { case l_false: TRACE("arith", tout << "propagation conflict\n";);