Checking cspFiles/BUF3.csp

Checking Test(inter(inputs(BUF3),outputs(BUF3)) == {}) [T= ERROR
xtrue
BEGIN TRACE example=0 process=1
error
END TRACE example=0 process=1

Checking HideAll(BUF3) :[divergence free [FD]]
xtrue
BEGIN TRACE example=0 process=0

END TRACE example=0 process=0

Checking BUF3 :[divergence free [FD]]
true

Checking LHS_InputDet(BUF3) [F= RHS_InputDet(BUF3)
true

Checking LHS_OutputDec_A(BUF3) [F= RHS_OutputDec_A(BUF3)
true

Checking LHS_OutputDec_B(BUF3,write3) [F= RHS_OutputDec_B(BUF3,write3)
true

Checking LHS_OutputDec_B(BUF3,read3) [F= RHS_OutputDec_B(BUF3,read3)
true