Fix semicolon_if_nothing_returned lints.

z3/src/config.rs

@@ -47,7 +47,7 @@ impl Config {
                 self.z3_cfg,
                 self.kvs.last().unwrap().0.as_ptr(),
                 self.kvs.last().unwrap().1.as_ptr(),
-            )
+            );
         };
     }
 

z3/src/context.rs

@@ -19,7 +19,7 @@ impl Context {
 
     /// Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
     pub fn interrupt(&self) {
-        self.handle().interrupt()
+        self.handle().interrupt();
     }
 
     /// Obtain a handle that can be used to interrupt computation from another thread.
@@ -51,7 +51,7 @@ impl Context {
     ///
     /// - [`Context::update_param_value()`]
     pub fn update_bool_param_value(&mut self, k: &str, v: bool) {
-        self.update_param_value(k, if v { "true" } else { "false" })
+        self.update_param_value(k, if v { "true" } else { "false" });
     }
 }
 

z3/src/datatype_builder.rs

@@ -176,7 +176,7 @@ pub fn create_datatypes<'ctx>(
             });
         }
 
-        datatype_sorts.push(DatatypeSort { sort, variants })
+        datatype_sorts.push(DatatypeSort { sort, variants });
     }
 
     for ctor in ctors {

z3/src/func_interp.rs

@@ -35,7 +35,7 @@ impl<'ctx> FuncInterp<'ctx> {
             args.iter()
                 .for_each(|a| Z3_ast_vector_push(self.ctx.z3_ctx, v, a.z3_ast));
 
-            Z3_func_interp_add_entry(self.ctx.z3_ctx, self.z3_func_interp, v, value.z3_ast)
+            Z3_func_interp_add_entry(self.ctx.z3_ctx, self.z3_func_interp, v, value.z3_ast);
         }
     }
 
@@ -74,7 +74,7 @@ impl<'ctx> fmt::Display for FuncInterp<'ctx> {
         self.get_entries().into_iter().try_for_each(|e| {
             let n = e.get_num_args();
             if n > 1 {
-                write!(f, "[")?
+                write!(f, "[")?;
             };
             write!(
                 f,
@@ -86,7 +86,7 @@ impl<'ctx> fmt::Display for FuncInterp<'ctx> {
                     .join(", ")
             )?;
             if n > 1 {
-                write!(f, "]")?
+                write!(f, "]")?;
             }
             write!(f, " -> {}, ", e.get_value())
         })?;

z3/src/params.rs

@@ -22,7 +22,7 @@ impl<'ctx> Params<'ctx> {
                 self.z3_params,
                 k.into().as_z3_symbol(self.ctx),
                 v.into().as_z3_symbol(self.ctx),
-            )
+            );
         };
     }
 
@@ -33,7 +33,7 @@ impl<'ctx> Params<'ctx> {
                 self.z3_params,
                 k.into().as_z3_symbol(self.ctx),
                 v,
-            )
+            );
         };
     }
 
@@ -44,7 +44,7 @@ impl<'ctx> Params<'ctx> {
                 self.z3_params,
                 k.into().as_z3_symbol(self.ctx),
                 v,
-            )
+            );
         };
     }
 
@@ -55,7 +55,7 @@ impl<'ctx> Params<'ctx> {
                 self.z3_params,
                 k.into().as_z3_symbol(self.ctx),
                 v,
-            )
+            );
         };
     }
 }

z3/tests/lib.rs

@@ -528,7 +528,7 @@ fn test_string_eq() {
     assert_eq!(solver.check(), SatResult::Sat);
 
     solver.assert(&h._eq(&z));
-    assert_eq!(solver.check(), SatResult::Unsat)
+    assert_eq!(solver.check(), SatResult::Unsat);
 }
 
 #[test]
@@ -542,7 +542,7 @@ fn test_string_concat() {
     let z = ast::String::from_str(&ctx, "foobar").unwrap();
 
     solver.assert(&ast::String::concat(&ctx, &[&x, &y])._eq(&z));
-    assert_eq!(solver.check(), SatResult::Sat)
+    assert_eq!(solver.check(), SatResult::Sat);
 }
 
 #[test]
@@ -555,7 +555,7 @@ fn test_string_prefix() {
     let y = ast::String::from_str(&ctx, "foobar").unwrap();
 
     solver.assert(&x.prefix(&y));
-    assert_eq!(solver.check(), SatResult::Sat)
+    assert_eq!(solver.check(), SatResult::Sat);
 }
 
 #[test]
@@ -568,7 +568,7 @@ fn test_string_suffix() {
     let y = ast::String::from_str(&ctx, "foobar").unwrap();
 
     solver.assert(&x.suffix(&y));
-    assert_eq!(solver.check(), SatResult::Sat)
+    assert_eq!(solver.check(), SatResult::Sat);
 }
 
 fn assert_string_roundtrip(source: &str) {
@@ -615,7 +615,7 @@ fn test_rec_func_def() {
     solver.assert(&y._eq(&fac.apply(&[&ast::Int::from_i64(&ctx, 5)]).as_int().unwrap()));
     solver.assert(&y._eq(&ast::Int::from_i64(&ctx, 120)));
 
-    assert_eq!(solver.check(), SatResult::Sat)
+    assert_eq!(solver.check(), SatResult::Sat);
 }
 
 #[test]
@@ -650,7 +650,7 @@ fn test_rec_func_def_unsat() {
     // To see this, comment out `fac.add_def(&[&n.into()], &body);`
     solver.assert(&y._eq(&ast::Int::from_i64(&ctx, 25)));
 
-    assert_eq!(solver.check(), SatResult::Unsat)
+    assert_eq!(solver.check(), SatResult::Unsat);
 }
 
 #[test]
@@ -1781,5 +1781,5 @@ fn iterate_all_solutions() {
             ]
             .into_iter()
             .collect()
-    )
+    );
 }

z3/tests/semver_tests.rs

@@ -163,14 +163,14 @@ fn test_solve_simple_semver_example() {
             None => (),
             Some(low) => {
                 info!("Asserting: {} >= #{} (root)", k, low);
-                opt.assert(&ast.ge(&ast::Int::from_u64(&ctx, low as u64)))
+                opt.assert(&ast.ge(&ast::Int::from_u64(&ctx, low as u64)));
             }
         }
         match last_version_req_index(&smap, k, v) {
             None => (),
             Some(high) => {
                 info!("Asserting: {} <= #{} (root)", k, high);
-                opt.assert(&ast.le(&ast::Int::from_u64(&ctx, high as u64)))
+                opt.assert(&ast.le(&ast::Int::from_u64(&ctx, high as u64)));
             }
         }
         asts.insert(k.clone(), ast);
@@ -224,7 +224,7 @@ fn test_solve_simple_semver_example() {
                             &k_ast
                                 ._eq(&ast::Int::from_u64(&ctx, n as u64))
                                 .implies(&r_ast.ge(&ast::Int::from_u64(&ctx, low as u64))),
-                        )
+                        );
                     }
                 }
                 match last_version_req_index(&smap, r, req) {
@@ -243,7 +243,7 @@ fn test_solve_simple_semver_example() {
                             &k_ast
                                 ._eq(&ast::Int::from_u64(&ctx, n as u64))
                                 .implies(&r_ast.le(&ast::Int::from_u64(&ctx, high as u64))),
-                        )
+                        );
                     }
                 }
             }