id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
14	flaw in simplify routine?	Stephen Siegel	ywei	"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;
			}
		}"	defect	closed	major		symbolic	1.0	fixed