Move most of SMTChecker tests from C++ to isoltest

But keep divison in C++ because results differ between different solvers

1 files changed, 12 insertions, 0 deletions

diff --git a/test/libsolidity/smtCheckerTests/037_while_loop_simple.sol b/test/libsolidity/smtCheckerTests/037_while_loop_simple.sol
new file mode 100644
index 00000000..41559c99
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/037_while_loop_simple.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+// Check that side-effects of condition are taken into account
+contract C {
+    function f(uint x, uint y) public pure {
+        x = 7;
+        while ((x = y) > 0) {
+        }
+        assert(x == 7);
+    }
+}
+// ----
+// Warning: (216-230): Assertion violation happens here\nNote that some information is erased after the execution of loops.\nYou can re-introduce information using require().