diff --git a/src/smt/theory_arith_inv.h b/src/smt/theory_arith_inv.h index 987d075c3..12dd0bb38 100644 --- a/src/smt/theory_arith_inv.h +++ b/src/smt/theory_arith_inv.h @@ -215,6 +215,8 @@ namespace smt { template bool theory_arith::valid_assignment() const { + if (get_manager().canceled()) + return true; if (valid_row_assignment() && satisfy_bounds() && satisfy_integrality()) {