diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index 51ba2fc98..c8f6c2581 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -2796,6 +2796,9 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uin // Analysis might have discovered base level conflict if (mcsat->status == STATUS_UNSAT) { + if (n_assumptions == 0) { + mcsat->interpolant = false_term; + } break; }