From d8d06360ac4b5296c071307a41123ef1938e9275 Mon Sep 17 00:00:00 2001
From: "Jip J. Dekker" <jip@dekker.one>
Date: Wed, 3 Apr 2024 15:26:43 +1100
Subject: [PATCH] Rectify invalid assumption in the IPASIR-UP's check model
 callback

---
 crates/pindakaas/src/solver.rs            |  4 +---
 crates/pindakaas/src/solver/libloading.rs | 16 +++++-----------
 2 files changed, 6 insertions(+), 14 deletions(-)

diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs
index b84574b51..30055537f 100644
--- a/crates/pindakaas/src/solver.rs
+++ b/crates/pindakaas/src/solver.rs
@@ -254,9 +254,7 @@ impl VarFactory {
 
 	/// Return the next [`size`] variables that can be stored as an inclusive range.
 	pub fn new_var_range(&mut self, size: usize) -> Option<VarRange> {
-		let Some(start) = self.next_var else {
-			return None;
-		};
+		let start = self.next_var?;
 		match size {
 			0 => Some(VarRange::new(
 				Var(NonZeroI32::new(2).unwrap()),
diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs
index d6ae4ba7a..1a471c00e 100644
--- a/crates/pindakaas/src/solver/libloading.rs
+++ b/crates/pindakaas/src/solver/libloading.rs
@@ -376,17 +376,11 @@ pub(crate) unsafe extern "C" fn ipasir_check_model_cb(
 ) -> bool {
 	let prop = &mut *(state as *mut IpasirPropStore);
 	let sol = std::slice::from_raw_parts(model, len);
-	let value = |l: Lit| {
-		let abs: Lit = l.var().into();
-		let v = Into::<i32>::into(abs) as usize;
-		if v <= sol.len() {
-			// TODO: is this correct here?
-			debug_assert_eq!(sol[v - 1].abs(), l.var().into());
-			Some(sol[v - 1] == l.into())
-		} else {
-			None
-		}
-	};
+	let sol: std::collections::HashMap<Var, bool> = sol
+		.iter()
+		.map(|&i| (Var(NonZeroI32::new(i.abs()).unwrap()), i >= 0))
+		.collect();
+	let value = |l: Lit| sol.get(&l.var()).copied();
 	prop.prop.check_model(&value)
 }
 #[cfg(feature = "ipasir-up")]