test: add div-by-zero semantics test

tests/expected/all.json

@@ -22,6 +22,24 @@
             }
         ],
         "test/Arith.t.sol:ArithTest": [
+            {
+                "name": "check_Div_fail(uint256,uint256)",
+                "exitcode": 1,
+                "num_models": 1,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_Div_pass(uint256,uint256)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
             {
                 "name": "check_Exp(uint256)",
                 "exitcode": 0,

tests/regression/test/Arith.t.sol

@@ -3,6 +3,12 @@ pragma solidity >=0.8.0 <0.9.0;
 
 contract ArithTest {
 
+    function unchecked_div(uint x, uint y) public pure returns (uint ret) {
+        assembly {
+            ret := div(x, y)
+        }
+    }
+
     function unchecked_mod(uint x, uint y) public pure returns (uint ret) {
         assembly {
             ret := mod(x, y)
@@ -34,4 +40,23 @@ contract ArithTest {
         //  assert(x ** 8 == (x ** 4) ** 2);
         }
     }
+
+    function check_Div_fail(uint x, uint y) public pure {
+        require(x > y);
+
+        uint q = unchecked_div(x, y);
+
+        // note: since x > y, q can be zero only when y == 0, due to the division-by-zero semantics in the EVM
+
+        assert(q != 0); // counterexample: y == 0
+    }
+
+    function check_Div_pass(uint x, uint y) public pure {
+        require(x > y);
+        require(y > 0);
+
+        uint q = unchecked_div(x, y);
+
+        assert(q != 0); // pass
+    }
 }