packages feed

sbv-6.0: SBVUnitTest/GoldFiles/basic-3_2.gold

INPUTS
  s0 :: SWord8, aliasing "x"
  s1 :: SWord8, aliasing "y"
CONSTANTS
  s_2 = False :: Bool
  s_1 = True :: Bool
TABLES
ARRAYS
UNINTERPRETED CONSTANTS
USER GIVEN CODE SEGMENTS
AXIOMS
TACTICS
GOALS
DEFINE
  s2 :: SWord8 = s0 * s0
  s3 :: SWord8 = s1 * s1
  s4 :: SWord8 = s2 - s3
CONSTRAINTS
ASSERTIONS
OUTPUTS
  s4