diff --git a/Test/prover/smt-options.bpl b/Test/prover/smt-options.bpl
new file mode 100644
index 000000000..8d4d8c8e8
--- /dev/null
+++ b/Test/prover/smt-options.bpl
@@ -0,0 +1,17 @@
+// RUN: %boogie /proverLog:"%t.smt2" "%s"
+// RUN: %OutputCheck --file-to-check "%t.smt2" "%s"
+// CHECK: (set-option :smt.arith.solver 2)
+// CHECK: (set-option :smt.arith.solver 6)
+// CHECK: (set-option :sat.smt.proof.check true)
+procedure
+{:smt_option "smt.arith.solver", 2}
+P1(a: int, b: int) {
+  assert (a + b) - (a * b) == (b + a) - (a * b);
+}
+
+procedure
+{:smt_option "smt.arith.solver", 6}
+{:smt_option "sat.smt.proof.check", true}
+P2(a: int, b: int) {
+  assert (a + b) - (a * b) == (b + a) - (a * b);
+}