id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
111	matmat compare: outputs not equivalent?	Stephen Siegel	ywei	"Running compare on matmat, everything seems fine until the end, when the results are compared.  Here is the command:
{{{
compare -simplify  -verbose /Users/siegel/Documents/workspace/MiniMP/examples/matmat/matmat-seq_1_1_2.mmp -np 1 /Users/siegel/Documents/workspace/MiniMP/examples/matmat/matmat-par_1_1_2.mmp -np 2
}}}

Here is the report that the two results may differ, but they look the same!:
{{{
Possible violation detected with specification at State 47
Possible incorrect final value for implementation output variable c at State 90.
Expected value: real[X2][X1]: matmat-seq_1_1_2_V5<(0, 0), (X3[0, 0]*X4[0, 0])><(1, 0), (X4[0, 0]*X3[0, 1])>
Actual value: real[X2][X1]: matmat-par_1_1_2_V5<(0, 0), (X3[0, 0]*X4[0, 0])><(1, 0), (X4[0, 0]*X3[0, 1])>
}}}

Here is the actual CVC3 query that returns false:
{{{
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: (FORALL (_BD1TY0: INT, _BD2TY0: INT): (LET cvc_1 = X3[0],
cvc_2 = X4[0][0],
cvc_7 = (cvc_1[0] * cvc_2),
cvc_5 = (cvc_2 * cvc_1[1]),
cvc_9 = (_BD2TY0 * -1),
cvc_6 = (_BD2TY0 = 0),
cvc_0 = (_BD1TY0 = 0),
cvc_4 = ((cvc_9 + 1) = 0),
cvc_3 = matmat-seq_1_1_2_V5[_BD1TY0],
cvc_8 = matmat-par_1_1_2_V5[_BD1TY0]
IN ((IF cvc_4 THEN IF cvc_0 THEN cvc_5 ELSE cvc_3[1] ENDIF ELSE IF cvc_6 THEN IF cvc_0 THEN cvc_7 ELSE cvc_3[0] ENDIF ELSE cvc_3[_BD2TY0] ENDIF ENDIF = IF cvc_4 THEN IF cvc_0 THEN cvc_5 ELSE cvc_8[1] ENDIF ELSE IF cvc_6 THEN IF cvc_0 THEN cvc_7 ELSE cvc_8[0] ENDIF ELSE cvc_8[_BD2TY0] ENDIF ENDIF) OR NOT ((0 <= ((cvc_9 + -1) + X2)) AND ((0 <= _BD2TY0) AND ((0 <= (((_BD1TY0 * -1) + -1) + X2)) AND (0 <= _BD1TY0))))))) under context ((0 <= (X2 + -2)) AND ((0 <= (X0 + -1)) AND ((0 <= (X1 + -1)) AND ((0 <= (X2 + -1)) AND ((0 <= ((X2 * -1) + 2)) AND ((0 <= X2) AND ((0 <= ((X1 * -1) + 1)) AND ((0 <= X1) AND ((0 <= ((X0 * -1) + 1)) AND (0 <= X0)))))))))) 
Invalid
}}}

Any ideas what is going on?
"	defect	closed	major		Administration	1.0	fixed