WIP before core rewrite

1 files changed, 10 insertions, 10 deletions

diff --git a/z3-solver/src/lib.rs b/z3-solver/src/lib.rs
index 04d77eb..35a17a8 100644
--- a/z3-solver/src/lib.rs
+++ b/z3-solver/src/lib.rs
@@ -45,7 +45,7 @@ impl<'z3> Z3Context<'z3> {
     pub fn new(ctx: &'z3 z3::Context) -> Self {
         Self {
             ctx,
-            solver: z3::Solver::new(&ctx),
+            solver: z3::Solver::new(ctx),
             floats: HashMap::new(),
             max_float_id: 0,
             bools: HashMap::new(),
@@ -85,7 +85,7 @@ impl<'z3> Z3Context<'z3> {
         let handle = match f {
             Float::Fixed(value) => {
                 let (num, den) = value_to_num_den(value);
-                return z3::ast::Real::from_real(&self.ctx, num, den);
+                return z3::ast::Real::from_real(self.ctx, num, den);
             }
             Float::Variable(handle) => handle,
         };
@@ -128,7 +128,7 @@ impl<'z3> SolverContext for Z3Context<'z3> {
         let id = self.max_float_id;
         let handle = VariableHandle::new(id as usize);
         self.floats
-            .insert(handle, z3::ast::Real::new_const(&self.ctx, id));
+            .insert(handle, z3::ast::Real::new_const(self.ctx, id));
         Float::from_handle(handle)
     }
 
@@ -140,7 +140,7 @@ impl<'z3> SolverContext for Z3Context<'z3> {
         let (num, den) = value_to_num_den(value);
 
         self.floats
-            .insert(handle, z3::ast::Real::from_real(&self.ctx, num, den));
+            .insert(handle, z3::ast::Real::from_real(self.ctx, num, den));
         Float::from_handle(handle)
     }
 
@@ -236,7 +236,7 @@ impl<'z3> SolverContext for Z3Context<'z3> {
         let id = self.max_bool_id;
         let handle = VariableHandle::new(id as usize);
         self.bools
-            .insert(handle, z3::ast::Bool::new_const(&self.ctx, id));
+            .insert(handle, z3::ast::Bool::new_const(self.ctx, id));
         Bool::new(handle)
     }
 
@@ -246,21 +246,21 @@ impl<'z3> SolverContext for Z3Context<'z3> {
         let handle = VariableHandle::new(id as usize);
 
         self.bools
-            .insert(handle, z3::ast::Bool::from_bool(&self.ctx, value));
+            .insert(handle, z3::ast::Bool::from_bool(self.ctx, value));
         Bool::new(handle)
     }
 
     fn bool_eq(&mut self, lhs: Bool, rhs: Bool) -> Bool {
         let lhs = self.bool(lhs);
         let rhs = self.bool(rhs);
-        let result = lhs._eq(&rhs);
+        let result = lhs._eq(rhs);
         self.anon_bool(result)
     }
 
     fn bool_ne(&mut self, lhs: Bool, rhs: Bool) -> Bool {
         let lhs = self.bool(lhs);
         let rhs = self.bool(rhs);
-        let result = lhs._eq(&rhs).not();
+        let result = lhs._eq(rhs).not();
         self.anon_bool(result)
     }
 
@@ -308,7 +308,7 @@ impl SolverModel for Z3Model<'_> {
 
         let (num, den) = self
             .model
-            .eval::<z3::ast::Real>(self.ctx.floats.get(&handle).expect("Couldn't find float"))
+            .eval::<z3::ast::Real>(self.ctx.floats.get(&handle).expect("Couldn't find float"), true)
             .unwrap()
             .as_real()
             .unwrap();
@@ -319,7 +319,7 @@ impl SolverModel for Z3Model<'_> {
     fn eval_bool(&self, f: Bool) -> Option<bool> {
         Some(
             self.model
-                .eval::<z3::ast::Bool>(&self.ctx.bool(f))
+                .eval::<z3::ast::Bool>(self.ctx.bool(f), true)
                 .unwrap()
                 .as_bool()
                 .unwrap(),