Set the default error handler to None

z3/src/ast.rs

@@ -645,7 +645,7 @@ impl<'ctx> Int<'ctx> {
     /// let x = ast::Int::from_bv(&bv, true);
     ///
     /// assert_eq!(solver.check(), SatResult::Sat);
-    /// let model = solver.get_model();
+    /// let model = solver.get_model().unwrap();
     ///
     /// assert_eq!(-3, model.eval(&x).unwrap().as_i64().unwrap());
     /// ```
@@ -932,7 +932,7 @@ impl<'ctx> BV<'ctx> {
     /// assert_eq!(64, x.get_size());
     ///
     /// assert_eq!(solver.check(), SatResult::Sat);
-    /// let model = solver.get_model();
+    /// let model = solver.get_model().unwrap();;
     ///
     /// assert_eq!(-3, model.eval(&x.to_int(true)).unwrap().as_i64().expect("as_i64() shouldn't fail"));
     /// ```
@@ -1407,7 +1407,7 @@ impl<'ctx> Datatype<'ctx> {
 /// solver.assert(&forall);
 ///
 /// assert_eq!(solver.check(), SatResult::Sat);
-/// let model = solver.get_model();
+/// let model = solver.get_model().unwrap();;
 ///
 /// let f_f_3: ast::Int = f.apply(&[&f.apply(&[&ast::Int::from_u64(&ctx, 3).into()])]).try_into().unwrap();
 /// assert_eq!(3, model.eval(&f_f_3).unwrap().as_u64().unwrap());
@@ -1466,7 +1466,7 @@ pub fn forall_const<'ctx>(
 /// solver.assert(&exists.not());
 ///
 /// assert_eq!(solver.check(), SatResult::Sat);
-/// let model = solver.get_model();
+/// let model = solver.get_model().unwrap();;
 ///
 /// let f_f_3: ast::Int = f.apply(&[&f.apply(&[&ast::Int::from_u64(&ctx, 3).into()])]).try_into().unwrap();
 /// assert_eq!(3, model.eval(&f_f_3).unwrap().as_u64().unwrap());

z3/src/context.rs

@@ -10,6 +10,7 @@ impl Context {
                 let guard = Z3_MUTEX.lock().unwrap();
                 let p = Z3_mk_context_rc(cfg.z3_cfg);
                 debug!("new context {:p}", p);
+                Z3_set_error_handler(p, None);
                 p
             },
         }

z3/src/lib.rs

@@ -151,7 +151,7 @@ pub struct FuncDecl<'ctx> {
 /// solver.assert(&y._eq(&value.as_datatype().unwrap()));
 ///
 /// assert_eq!(solver.check(), SatResult::Sat);
-/// let model = solver.get_model();
+/// let model = solver.get_model().unwrap();;
 ///
 /// // Get the value out of Some(3)
 /// let ast = option_int.variants[1].accessors[0].apply(&[&y.into()]);

z3/src/model.rs

@@ -9,28 +9,34 @@ use Solver;
 use Z3_MUTEX;
 
 impl<'ctx> Model<'ctx> {
-    pub fn of_solver(slv: &Solver<'ctx>) -> Model<'ctx> {
-        Model {
+    pub fn of_solver(slv: &Solver<'ctx>) -> Option<Model<'ctx>> {
+        Some(Model {
             ctx: slv.ctx,
             z3_mdl: unsafe {
                 let guard = Z3_MUTEX.lock().unwrap();
                 let m = Z3_solver_get_model(slv.ctx.z3_ctx, slv.z3_slv);
+                if m.is_null() {
+                    return None;
+                }
                 Z3_model_inc_ref(slv.ctx.z3_ctx, m);
                 m
             },
-        }
+        })
     }
 
-    pub fn of_optimize(opt: &Optimize<'ctx>) -> Model<'ctx> {
-        Model {
+    pub fn of_optimize(opt: &Optimize<'ctx>) -> Option<Model<'ctx>> {
+        Some(Model {
             ctx: opt.ctx,
             z3_mdl: unsafe {
                 let guard = Z3_MUTEX.lock().unwrap();
                 let m = Z3_optimize_get_model(opt.ctx.z3_ctx, opt.z3_opt);
+                if m.is_null() {
+                    return None;
+                }
                 Z3_model_inc_ref(opt.ctx.z3_ctx, m);
                 m
             },
-        }
+        })
     }
 
     /// Translate model to context `dest`
@@ -96,3 +102,14 @@ impl<'ctx> Drop for Model<'ctx> {
         unsafe { Z3_model_dec_ref(self.ctx.z3_ctx, self.z3_mdl) };
     }
 }
+
+#[test]
+fn test_unsat() {
+    use crate::{ast, Config, SatResult};
+    let cfg = Config::new();
+    let ctx = Context::new(&cfg);
+    let solver = Solver::new(&ctx);
+    solver.assert(&ast::Bool::from_bool(&ctx, false));
+    assert_eq!(solver.check(), SatResult::Unsat);
+    assert!(solver.get_model().is_none());
+}

z3/src/optimize.rs

@@ -113,7 +113,7 @@ impl<'ctx> Optimize<'ctx> {
     /// The error handler is invoked if a model is not available because
     /// the commands above were not invoked for the given optimization
     /// solver, or if the result was `Z3_L_FALSE`.
-    pub fn get_model(&self) -> Model<'ctx> {
+    pub fn get_model(&self) -> Option<Model<'ctx>> {
         Model::of_optimize(self)
     }
 

z3/src/solver.rs

@@ -247,7 +247,7 @@ impl<'ctx> Solver<'ctx> {
     /// The error handler is invoked if a model is not available because
     /// the commands above were not invoked for the given solver, or if
     /// the result was `Z3_L_FALSE`.
-    pub fn get_model(&self) -> Model<'ctx> {
+    pub fn get_model(&self) -> Option<Model<'ctx>> {
         Model::of_solver(self)
     }
 
@@ -266,11 +266,15 @@ impl<'ctx> Solver<'ctx> {
     //
     // This seems to actually return an Ast with kind `SortKind::Unknown`, which we don't
     // have an Ast subtype for yet.
-    pub fn get_proof(&self) -> impl Ast<'ctx> {
+    pub fn get_proof(&self) -> Option<impl Ast<'ctx>> {
         let guard = Z3_MUTEX.lock().unwrap();
-        ast::Dynamic::new(self.ctx, unsafe {
-            Z3_solver_get_proof(self.ctx.z3_ctx, self.z3_slv)
-        })
+        Some(ast::Dynamic::new(self.ctx, unsafe {
+            let m = Z3_solver_get_proof(self.ctx.z3_ctx, self.z3_slv);
+            if m.is_null() {
+                return None;
+            }
+            m
+        }))
     }
 
     /// Return a brief justification for an "unknown" result (i.e., `SatResult::Unknown`) for

z3/src/sort.rs

@@ -83,7 +83,7 @@ impl<'ctx> Sort<'ctx> {
     /// let eq = red_tester.apply(&[&red_const]);
     ///
     /// assert_eq!(solver.check(), SatResult::Sat);
-    /// let model = solver.get_model();
+    /// let model = solver.get_model().unwrap();;
     ///
     /// assert!(model.eval(&eq).unwrap().as_bool().unwrap().as_bool().unwrap());
     /// ```

z3/tests/lib.rs

@@ -72,7 +72,7 @@ fn test_solving_for_model() {
     solver.assert(&x_plus_two.gt(&seven));
     assert_eq!(solver.check(), SatResult::Sat);
 
-    let model = solver.get_model();
+    let model = solver.get_model().unwrap();
     let xv = model.eval(&x).unwrap().as_i64().unwrap();
     let yv = model.eval(&y).unwrap().as_i64().unwrap();
     info!("x: {}", xv);
@@ -95,7 +95,7 @@ fn test_cloning_ast() {
     solver.assert(&x._eq(&zero));
     assert_eq!(solver.check(), SatResult::Sat);
 
-    let model = solver.get_model();
+    let model = solver.get_model().unwrap();
     let xv = model.eval(&x).unwrap().as_i64().unwrap();
     let yv = model.eval(&y).unwrap().as_i64().unwrap();
     assert_eq!(xv, 0);
@@ -128,7 +128,7 @@ fn test_bitvectors() {
     solver.assert(&b_plus_two.bvsgt(&a));
     assert_eq!(solver.check(), SatResult::Sat);
 
-    let model = solver.get_model();
+    let model = solver.get_model().unwrap();
     let av = model.eval(&a).unwrap().as_i64().unwrap();
     let bv = model.eval(&b).unwrap().as_i64().unwrap();
     assert!(av > bv);
@@ -186,7 +186,7 @@ fn test_model_translate() {
     slv.assert(&a._eq(&ast::Int::from_u64(&source, 2)));
     assert_eq!(slv.check(), SatResult::Sat);
 
-    let model = slv.get_model();
+    let model = slv.get_model().unwrap();
     assert_eq!(2, model.eval(&a).unwrap().as_i64().unwrap());
     let translated_model = model.translate(&destination);
     assert_eq!(2, translated_model.eval(&translated_a).unwrap().as_i64().unwrap());
@@ -203,7 +203,7 @@ fn test_pb_ops_model() {
 
     solver.assert(&ast::Bool::pb_eq(&ctx, &[(&x, 1), (&y, 1)], 1));
     assert_eq!(solver.check(), SatResult::Sat);
-    let model = solver.get_model();
+    let model = solver.get_model().unwrap();
     let xv = model.eval(&x).unwrap().as_bool().unwrap();
     let yv = model.eval(&y).unwrap().as_bool().unwrap();
     info!("x: {}", xv);
@@ -214,7 +214,7 @@ fn test_pb_ops_model() {
     solver.push();
     solver.assert(&ast::Bool::pb_ge(&ctx, &[(&x, 1), (&y, 1)], 2));
     assert_eq!(solver.check(), SatResult::Sat);
-    let model = solver.get_model();
+    let model = solver.get_model().unwrap();
     let xv = model.eval(&x).unwrap().as_bool().unwrap();
     let yv = model.eval(&y).unwrap().as_bool().unwrap();
     info!("x: {}", xv);
@@ -224,7 +224,7 @@ fn test_pb_ops_model() {
     solver.pop(1);
     solver.assert(&ast::Bool::pb_le(&ctx, &[(&x, 1), (&y, 1)], 0));
     assert_eq!(solver.check(), SatResult::Sat);
-    let model = solver.get_model();
+    let model = solver.get_model().unwrap();
     let xv = model.eval(&x).unwrap().as_bool().unwrap();
     let yv = model.eval(&y).unwrap().as_bool().unwrap();
     info!("x: {}", xv);
@@ -563,3 +563,11 @@ fn test_datatype_builder() {
 
     assert_eq!(solver.check(), SatResult::Sat);
 }
+
+#[test]
+fn get_model_without_check_does_not_exit() {
+    let cfg = Config::new();
+    let ctx = Context::new(&cfg);
+    let solver = Solver::new(&ctx);
+    solver.get_model();
+}

z3/tests/semver_tests.rs

@@ -270,7 +270,7 @@ fn test_solve_simple_semver_example() {
     }
 
     assert_eq!(opt.check(&[]), SatResult::Sat);
-    let model = opt.get_model();
+    let model = opt.get_model().unwrap();
 
     for k in root.keys() {
         let ast = &asts[k];