From 644d02d51a44c723e97f03cd572a2b43cb34766c Mon Sep 17 00:00:00 2001
From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com>
Date: Wed, 17 Apr 2024 00:18:53 -0700
Subject: [PATCH] false_term as interpolant when assumptions are empty

---
 src/mcsat/solver.c | 3 +++
 1 file changed, 3 insertions(+)

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;
     }