diff --git a/test/formal/sub_not_zero_x_to_not_x_256.py b/test/formal/sub_not_zero_x_to_not_x_256.py new file mode 100644 index 000000000..eb3301100 --- /dev/null +++ b/test/formal/sub_not_zero_x_to_not_x_256.py @@ -0,0 +1,26 @@ +from rule import Rule +from opcodes import * + +""" +Rule: +SUB(~0, X) -> NOT(X) +Requirements: +""" + +rule = Rule() + +n_bits = 256 + +# Input vars +X = BitVec('X', n_bits) + +# Constants +ZERO = BitVecVal(0, n_bits) + +# Non optimized result +nonopt = SUB(~ZERO, X) + +# Optimized result +opt = NOT(X) + +rule.check(nonopt, opt)