test case for #3

yav · Aug 15, 2022 · 21571e9 · 21571e9
1 parent 3cc737d
commit 21571e9
Showing 1 changed file with 14 additions and 0 deletions.
diff --git a/examples/ex2.hs b/examples/ex2.hs
@@ -0,0 +1,14 @@
+import SimpleSMT
+
+main :: IO ()
+main =
+  do l <- newLogger 0
+     s <- newSolver "z3" [ "-in", "-smt2" ] (Just l)
+     setLogic s "QF_LRA"
+     x <- declare s "x" tReal
+     assert s (mul (real 3) (add x (real 2)) `eq` real 5)
+     print =<< check s
+     print =<< getExprs s [x]
+
+
+