Noise-1.0.1: Temp/sbv-0.9.18/SBVUnitTest/GoldFiles/basic-2_2.gold
INPUTS s0 :: SWord8, aliasing "y" CONSTANTS s_2 = False s_1 = True s1 = 9 :: SWord8 TABLES ARRAYS UNINTERPRETED CONSTANTS AXIOMS DEFINE s2 :: SWord8 = s0 * s0 s3 :: SWord8 = s1 - s2 OUTPUTS s3