Support for ** on ints

src/nagini_translation/resources/bool.sil

@@ -221,6 +221,24 @@ function int___mul__(self: Int, other: Int): Int
     self * other
 }
 
+function int___pow__(self: Int, other: Int): Int
+    decreases _
+    requires other >= 0
+{
+    ___pow(self, other)
+}
+
+domain ____pow_helper {
+  function ___pow(Int, Int): Int
+  axiom {
+    forall i1: Int :: { ___pow(i1, 0) } ___pow(i1, 0) == 1
+  }
+
+  axiom {
+    forall i1: Int, i2: Int :: { ___pow(i1, i2) } i2 > 0 ==> ___pow(i1, i2) == i1 * ___pow(i1, i2 - 1)
+  }
+}
+
 function int___floordiv__(self: Int, other: Int): Int
     decreases _
     requires @error("Divisor may be zero.")(other != 0)

src/nagini_translation/resources/builtins.json

@@ -241,6 +241,10 @@
             "args": ["__prim__int", "__prim__int"],
             "type": "__prim__int"
         },
+        "__pow__": {
+            "args": ["__prim__int", "__prim__int"],
+            "type": "__prim__int"
+        },
         "__truediv__": {
             "args": ["__prim__int", "__prim__int"],
             "type": "float"

tests/functional/verification/test_builtin_functions.py

@@ -11,6 +11,15 @@ def test_abs(x: int) -> None:
     #:: ExpectedOutput(assert.failed:assertion.false)
     assert abs(x) > 0
 
+def test_pow(x: int) -> None:
+    a = -2
+    b = a ** 0
+    assert b == 1
+    c = x ** 4
+    assert c == x * x * x * x
+    #:: ExpectedOutput(assert.failed:assertion.false)
+    assert 3 ** 2 == 8
+
 def test_max() -> None:
     assert max(1,max(-3, 6)) == 6
     c = max(2, -5) + max(-3, -2)