flaw in simplify routine?

[Stephen Siegel]

The following code occurs in SymUniverse.java, method andExpression. The problem is that if the result is already in the table, then the simplified result will not be returned. For example, if result is p&&p, then the first time this result is computed, p&&p will be entered into the table, and then the simplified version p will be entered into the table. The second time it is computed, p&&p will be found in the table and p&&p will be returned (instead of p).

I think the fix is to only enter the simplified version into the table.

if(this.exprTable.containsKey(result))
{

return this.exprTable.get(result);

}
else
{

this.exprTable.put(result, result);
SymExpression temp = this.prover.simplify(result);
if(!temp.equals(result))
{

this.exprTable.put(temp, temp);
return temp;

}
else
{

return result;

}

}

[ywei]

Fixed.