CL tests

Author: Leo Alt

test/cmdlineTests/model_checker_show_unproved_default_all_engines/args

@@ -0,0 +1 @@
+--model-checker-engine all

test/cmdlineTests/model_checker_show_unproved_default_all_engines/err

@@ -0,0 +1,3 @@
+Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
+
+Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.

test/cmdlineTests/model_checker_show_unproved_default_all_engines/input.sol

@@ -0,0 +1,12 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+contract C {
+    struct S {
+        uint x;
+    }
+    S s;
+    function f(bool b) public {
+        s.x |= b ? 1 : 2;
+        assert(s.x > 0);
+    }
+}

test/cmdlineTests/model_checker_show_unproved_default_bmc/args

@@ -0,0 +1 @@
+--model-checker-engine bmc

test/cmdlineTests/model_checker_show_unproved_default_bmc/err

@@ -0,0 +1 @@
+Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.

test/cmdlineTests/model_checker_show_unproved_default_bmc/input.sol

@@ -0,0 +1,12 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+contract C {
+    struct S {
+        uint x;
+    }
+    S s;
+    function f(bool b) public {
+        s.x |= b ? 1 : 2;
+        assert(s.x > 0);
+    }
+}

test/cmdlineTests/model_checker_show_unproved_default_chc/args

@@ -0,0 +1 @@
+--model-checker-engine chc

test/cmdlineTests/model_checker_show_unproved_default_chc/err

@@ -0,0 +1 @@
+Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.

test/cmdlineTests/model_checker_show_unproved_default_chc/input.sol

@@ -0,0 +1,12 @@
+// SPDX-License-Identifier: GPL-3.0
+pragma solidity >=0.0;
+contract C {
+    struct S {
+        uint x;
+    }
+    S s;
+    function f(bool b) public {
+        s.x |= b ? 1 : 2;
+        assert(s.x > 0);
+    }
+}

test/cmdlineTests/model_checker_show_unproved_false_all_engines/args

@@ -0,0 +1 @@
+--model-checker-engine all --model-checker-show-unproved false