Add test

boogie-org · Nov 15, 2023 · 2777ecd · 2777ecd
1 parent 972c1e3
commit 2777ecd
Showing 1 changed file with 17 additions and 0 deletions.
diff --git a/Test/prover/smt-options.bpl 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);
+}