Rectify invalid assumption in the IPASIR-UP's check model callback

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()),

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")]