tests: add a test for smt_sync

FStarLang · Apr 10, 2023 · a3e5a5f · a3e5a5f
1 parent 0002214
commit a3e5a5f
Showing 1 changed file with 13 additions and 0 deletions.
diff --git a/tests/tactics/SMTSync.fst b/tests/tactics/SMTSync.fst
@@ -0,0 +1,13 @@
+module SMTSync
+
+open FStar.Tactics
+
+let test1 x = assert (1 + x == x + 1)
+  by (try smt_sync () with |_ -> fail "")
+
+[@@expect_failure]
+let test2 x = assert (1 + x == x + 2)
+  by (try smt_sync () with |_ -> fail "")
+
+let test3 x = assert (1 + x == x + 2)
+  by (try smt_sync () with |_ -> tadmit ())