diff --git a/z3/src/ast.rs b/z3/src/ast.rs index c669d83c..4a60e19b 100644 --- a/z3/src/ast.rs +++ b/z3/src/ast.rs @@ -389,8 +389,8 @@ pub trait Ast<'ctx>: fmt::Debug { /// Return the `FuncDecl` of the `Ast`. /// - /// This will panic if the `Ast` is not an app, i.e. if AstKind is not App - /// or Numeral. + /// This will panic if the `Ast` is not an app, i.e. if [`AstKind`] is not + /// [`AstKind::App`] or [`AstKind::Numeral`]. fn decl(&self) -> FuncDecl<'ctx> { self.safe_decl().expect("Ast is not an app") } diff --git a/z3/src/model.rs b/z3/src/model.rs index 8cfaea08..40a28189 100644 --- a/z3/src/model.rs +++ b/z3/src/model.rs @@ -165,7 +165,7 @@ impl<'ctx> Drop for Model<'ctx> { } #[derive(Debug)] -/// https://z3prover.github.io/api/html/classz3py_1_1_model_ref.html#a7890b7c9bc70cf2a26a343c22d2c8367 +/// pub struct ModelIter<'ctx> { model: &'ctx Model<'ctx>, idx: u32, diff --git a/z3/tests/lib.rs b/z3/tests/lib.rs index 3028a3e9..35d60a8d 100644 --- a/z3/tests/lib.rs +++ b/z3/tests/lib.rs @@ -1619,7 +1619,7 @@ fn test_regex_capital_foobar_intersect_az_plus_is_unsat() { } #[test] -/// https://github.com/Z3Prover/z3/blob/21e59f7c6e5033006265fc6bc16e2c9f023db0e8/examples/dotnet/Program.cs#L329-L370 +/// fn test_array_example1() { let cfg = Config::new(); let ctx = &Context::new(&cfg); @@ -1671,7 +1671,7 @@ fn test_array_example1() { } #[test] -/// https://z3prover.github.io/api/html/classz3py_1_1_func_entry.html +/// fn return_number_args_in_given_entry() { let cfg = Config::new(); let ctx = &Context::new(&cfg); @@ -1712,7 +1712,7 @@ fn return_number_args_in_given_entry() { } #[test] -/// https://stackoverflow.com/questions/13395391/z3-finding-all-satisfying-models +/// fn iterate_all_solutions() { let cfg = Config::new(); let ctx = &Context::new(&cfg);