fix: preproc generic cause triviality check

hopv · Jan 15, 2024 · 5e25561 · 5e25561
1 parent fb8d1b9
commit 5e25561
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/src/common/smt.rs b/src/common/smt.rs
@@ -1097,7 +1097,10 @@ impl<Parser: Copy> ClauseTrivialExt for Solver<Parser> {
                 if lhs.is_empty() {
                     Ok(Some(false))
                 } else {
-                    conj.try_is_unsat(self)
+                    match conj.try_is_unsat(self) {
+                        Ok(Some(true)) => Ok(Some(true)),
+                        _ => Ok(Some(false)),
+                    }
                 }
             }
         };