z3 finds counter example for exponentiation when there is none

[Mareikes]

in the machine

MACHINE ArithmeticLaws
VARIABLES x
INVARIANT
x:INTEGER &
(x>0 => 2**(10x) = 2(2**(10*x-1)))
INITIALISATION
x := -3
OPERATIONS
IncX = SELECT x<50 THEN x := x+1 END
END

we get a counter example for x=7. Apparently we can't handle exponents > 64

[wysiib]

the number is too large for Z3 to handle it correctly. in consequence, it reports unknown. the error is wrongly reported because of the missing handling for UNKNOWN return statuses. This is already reported in #59

[x-moe-x]

We have a passing test for this issue but the machine already fails for x = 1, and doesn't see that 2^10 = 2*2^9...

[wysiib]

which test machine are you referring to?