Bug in checking equivalence of array outputs

[zirkel]

When an output variable is an array, the output from the spec is currently being compared to itself rather than to the output from the impl. This may be a bug in the verify package.

[ywei]

What is the exact command line options you used?

[Stephen Siegel]

Also, can you please check in a very simple test demonstrating this defect.

[Stephen Siegel]

I believe the defect is in the symbolic package. In the class CVC3TheoremProver, in the method processEqualityExpr, it looks like variables leftRead and rightRead are both getting set to the left expression:

    		Expr leftRead = null;
    		Expr rightRead = null;
    		
    		for(int i = 0; i < boundVars.size(); i++)
    		{
    			if(leftRead == null)
    			{
    				leftRead = vc.readExpr(parseSymExpr(left), (Expr)(boundVars.get(i)));
    				rightRead = vc.readExpr(parseSymExpr(left), (Expr)(boundVars.get(i)));
    			}
    			else
    			{
    				leftRead = vc.readExpr(leftRead, (Expr)(boundVars.get(i)));
    				rightRead = vc.readExpr(rightRead, (Expr)(boundVars.get(i)));
    			}
    		}

[ywei]

Fixed.