1INPUTS
2 s0 :: SWord8, aliasing "x"
3CONSTANTS
4TABLES
5ARRAYS
6UNINTERPRETED CONSTANTS
7USER GIVEN CODE SEGMENTS
8AXIOMS
9DEFINE
10 s1 :: SWord8 = s0 + s0
11 s2 :: SWord8 = s0 - s0
12 s3 :: SWord8 = s1 * s2
13CONSTRAINTS
14ASSERTIONS
15OUTPUTS
16 s3