diff --git a/.gitignore b/.gitignore
index a31c86965494..e3acaeebb7b4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -72,6 +72,9 @@ package-lock.json
 ## Rustdoc GUI tests
 tests/rustdoc-gui/src/**.lock
 
+## Boogie files
+*.bpl
+
 # Before adding new lines, see the comment at the top.
 /.litani_cache_dir
 /.ninja_deps
diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh
index a49af4f8178c..aaada9442417 100755
--- a/scripts/kani-regression.sh
+++ b/scripts/kani-regression.sh
@@ -59,6 +59,7 @@ TESTS=(
     "smack kani"
     "cargo-kani cargo-kani"
     "cargo-ui cargo-kani"
+    "script-based-boogie exec"
     "kani-docs cargo-kani"
     "kani-fixme kani-fixme"
 )
diff --git a/tests/script-based-boogie/assign/config.yml b/tests/script-based-boogie/assign/config.yml
new file mode 100644
index 000000000000..2e9f6c922a1e
--- /dev/null
+++ b/tests/script-based-boogie/assign/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: gen_boogie_and_dump.sh
+expected: expected
diff --git a/tests/script-based-boogie/assign/expected b/tests/script-based-boogie/assign/expected
new file mode 100644
index 000000000000..325ead72edbc
--- /dev/null
+++ b/tests/script-based-boogie/assign/expected
@@ -0,0 +1,7 @@
+procedure
+  var x: bv32;
+  var y: bv32;
+  x := 1bv32;
+  y := x;
+  x := 2bv32;
+  assert
diff --git a/tests/script-based-boogie/assign/gen_boogie_and_dump.sh b/tests/script-based-boogie/assign/gen_boogie_and_dump.sh
new file mode 100755
index 000000000000..0233ad780871
--- /dev/null
+++ b/tests/script-based-boogie/assign/gen_boogie_and_dump.sh
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set +e
+
+# Delete any leftover Boogie files
+rm *.bpl
+
+echo "[TEST] Run verification..."
+kani -Zboogie test.rs
+
+cat *.bpl
diff --git a/tests/script-based-boogie/assign/test.rs b/tests/script-based-boogie/assign/test.rs
new file mode 100644
index 000000000000..0a76c736e2f7
--- /dev/null
+++ b/tests/script-based-boogie/assign/test.rs
@@ -0,0 +1,38 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! A simple test that checks that assignment statements and asserts are
+//! translated to Boogie correctly.
+//!
+//! The `expected` file checks some elements of the expected output Boogie.
+//!
+//! This is a possible Boogie output (which may change with MIR changes):
+//! ```
+//! // Procedures:
+//! procedure _RNvCshNorBqfmMTU_4test19check_assign_assert()
+//! {
+//!   var x: bv32;
+//!   var y: bv32;
+//!   var _4: bool;
+//!   var _5: bv32;
+//!   var _7: bool;
+//!   x := 1bv32;
+//!   y := x;
+//!   x := 2bv32;
+//!   _5 := x;
+//!   _4 := (_5 == 2bv32);
+//!   assert _4;
+//!   _7 := (y == 1bv32);
+//!   assert _7;
+//!   return;
+//! }
+//! ```
+
+#[kani::proof]
+fn check_assign_assert() {
+    let mut x = 1;
+    let y = x;
+    x = 2;
+    kani::assert(x == 2, "");
+    kani::assert(y == 1, "");
+}
diff --git a/tests/script-based-boogie/binop/config.yml b/tests/script-based-boogie/binop/config.yml
new file mode 100644
index 000000000000..2e9f6c922a1e
--- /dev/null
+++ b/tests/script-based-boogie/binop/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: gen_boogie_and_dump.sh
+expected: expected
diff --git a/tests/script-based-boogie/binop/expected b/tests/script-based-boogie/binop/expected
new file mode 100644
index 000000000000..9eba8d5c8148
--- /dev/null
+++ b/tests/script-based-boogie/binop/expected
@@ -0,0 +1,19 @@
+function {:bvbuiltin "bvslt"} $BvSignedLessThan<T>(lhs: T, rhs: T) returns (bool);
+
+function {:bvbuiltin "bvsgt"} $BvSignedGreaterThan<T>(lhs: T, rhs: T) returns (bool);
+
+function {:bvbuiltin "bvor"} $BvOr<T>(lhs: T, rhs: T) returns (T);
+
+procedure
+  var _1: bv32;
+  var _2: bv32;
+  var _4: bool;
+  var z: bv32;
+  var _7: bool;
+  _1 := 1bv32;
+  _2 := 2bv32;
+  _4 := $BvSignedGreaterThan(_2, _1);
+  assert _4;
+  z := $BvOr(_1, _2);
+  _7 := $BvSignedLessThan(_1, z);
+  assert _7;
diff --git a/tests/script-based-boogie/binop/gen_boogie_and_dump.sh b/tests/script-based-boogie/binop/gen_boogie_and_dump.sh
new file mode 100755
index 000000000000..0233ad780871
--- /dev/null
+++ b/tests/script-based-boogie/binop/gen_boogie_and_dump.sh
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set +e
+
+# Delete any leftover Boogie files
+rm *.bpl
+
+echo "[TEST] Run verification..."
+kani -Zboogie test.rs
+
+cat *.bpl
diff --git a/tests/script-based-boogie/binop/test.rs b/tests/script-based-boogie/binop/test.rs
new file mode 100644
index 000000000000..84e637ecad9c
--- /dev/null
+++ b/tests/script-based-boogie/binop/test.rs
@@ -0,0 +1,44 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! A simple test that checks that binary operations are translated to a
+//! function call to an SMT bv operator
+//!
+//! The `expected` file checks some elements of the expected output Boogie.
+//!
+//! This is a possible Boogie output (which may change with MIR changes):
+//! ```
+//! function {:bvbuiltin "bvslt"} $BvSignedLessThan<T>(lhs: T, rhs: T) returns (bool);
+//!
+//! function {:bvbuiltin "bvsgt"} $BvSignedGreaterThan<T>(lhs: T, rhs: T) returns (bool);
+//!
+//! function {:bvbuiltin "bvor"} $BvOr<T>(lhs: T, rhs: T) returns (T);
+//!
+//! // Procedures:
+//! procedure _RNvCshNorBqfmMTU_4test14check_binop_gt()
+//! {
+//!   var _1: bv32;
+//!   var _2: bv32;
+//!   var _4: bool;
+//!   var z: bv32;
+//!   var _7: bool;
+//!   _1 := 1bv32;
+//!   _2 := 2bv32;
+//!   _4 := $BvSignedGreaterThan(_2, _1);
+//!   assert _4;
+//!   z := $BvAnd(_1, _2);
+//!   _7 := $BvSignedLessThan(_1, z);
+//!   assert _7;
+//!   return;
+//! }
+//!
+//! ````
+
+#[kani::proof]
+fn check_binop_gt() {
+    let x = 1;
+    let y = 2;
+    kani::assert(y > x, "");
+    let z = x | y;
+    kani::assert(x < z, "");
+}