Class  Description 

FloatEqual 
Represents an invariant of == between two double scalars.

FloatGreaterEqual 
Represents an invariant of ≥ between two double scalars.

FloatGreaterThan 
Represents an invariant of > between two double scalars.

FloatLessEqual 
Represents an invariant of ≤ between two double scalars.

FloatLessThan 
Represents an invariant of < between two double scalars.

FloatNonEqual 
Represents an invariant of !

IntEqual 
Represents an invariant of == between two long scalars.

IntGreaterEqual 
Represents an invariant of ≥ between two long scalars.

IntGreaterThan 
Represents an invariant of > between two long scalars.

IntLessEqual 
Represents an invariant of ≤ between two long scalars.

IntLessThan 
Represents an invariant of < between two long scalars.

IntNonEqual 
Represents an invariant of !

LinearBinary 
Represents a Linear invariant between two long
scalars
x and y , of the form
ax + by + c = 0 . 
LinearBinaryCore  
LinearBinaryCoreFloat  
LinearBinaryFloat 
Represents a Linear invariant between two double
scalars
x and y , of the form
ax + by + c = 0 . 
NumericFloat 
Baseclass for binary numeric invariants.

NumericFloat.Divides 
Represents the divides without remainder invariant between
two double scalars.

NumericFloat.Square 
Represents the square invariant between
two double scalars.

NumericFloat.ZeroTrack 
Represents the zero tracks invariant between
two double scalars; that is, when
x is zero,
y is also zero. 
NumericInt 
Baseclass for binary numeric invariants.

NumericInt.BitwiseAndZero 
Represents the BitwiseAnd == 0 invariant between
two long scalars; that is,
x and y have no
bits in common. 
NumericInt.BitwiseComplement 
Represents the bitwise complement invariant between
two long scalars.

NumericInt.BitwiseSubset 
Represents the bitwise subset invariant between
two long scalars; that is, the bits of
y are a subset of the
bits of x . 
NumericInt.Divides 
Represents the divides without remainder invariant between
two long scalars.

NumericInt.ShiftZero 
Represents the ShiftZero invariant between
two long scalars;
that is,
x rightshifted by y
is always zero. 
NumericInt.Square 
Represents the square invariant between
two long scalars.

NumericInt.ZeroTrack 
Represents the zero tracks invariant between
two long scalars; that is, when
x is zero,
y is also zero. 
TwoFloat 
Base class for two variable double invariants.

TwoScalar 
Base class for two variable long invariants.
