From 41c6623460cb993076d00d88b9519b329fae0e9d Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Mon, 25 Sep 2023 11:24:35 +0200
Subject: [PATCH] fix: exit gracefully on unknown result

---
 src/data.rs | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

diff --git a/src/data.rs b/src/data.rs
index 380ab01..11bb4e6 100644
--- a/src/data.rs
+++ b/src/data.rs
@@ -1145,7 +1145,7 @@ impl Data {
     /// }
     /// ```
     pub fn check_unsat(&mut self) -> Res<bool> {
-        self.get_unsat_proof().map(|_| true)
+        self.try_get_unsat_proof().map(|opt| opt.is_some())
     }
 
     /// Retrieves a proof of unsat.
@@ -1182,8 +1182,19 @@ impl Data {
     /// }
     /// ```
     pub fn get_unsat_proof(&mut self) -> Res<crate::unsat_core::UnsatRes> {
+        if let Some(res) = self.try_get_unsat_proof()? {
+            Ok(res)
+        } else {
+            bail!("asked for unsat proof while learning data is not unsat")
+        }
+    }
+
+    pub fn try_get_unsat_proof(&mut self) -> Res<Option<crate::unsat_core::UnsatRes>> {
         self.propagate()?;
-        log_verb! { "learning data on unsat:\n{}", self.string_do(& (), |s| s.to_string()).unwrap() }
+        log_verb!(
+            "learning data on unsat:\n{}",
+            self.string_do(&(), |s| s.to_string()).unwrap(),
+        );
         for (pred, samples) in self.pos.index_iter() {
             for sample in samples {
                 for neg in &self.neg[pred] {
@@ -1198,12 +1209,12 @@ impl Data {
                         } else {
                             None
                         };
-                        return Ok(crate::unsat_core::UnsatRes::new(entry_points));
+                        return Ok(Some(crate::unsat_core::UnsatRes::new(entry_points)));
                     }
                 }
             }
         }
-        bail!("asked for unsat proof while learning data is not unsat")
+        Ok(None)
     }
 
     /// Propagates all staged samples.