Fix bvsle/bvule with negative polarity.

UnconstrainedVariableSimplifier.cpp

@@ -214,6 +214,7 @@ void UnconstrainedVariableSimplifier::SimplifyIte()
 	oldHash = expression.hash();
 
 	SimplifyOnce();
+
 	expression = expression.simplify();
 //	std::cout << "Simplify once" << std::endl;
 	//expression = simplifier.PushNegations(expression);
@@ -480,7 +481,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
 		    }
 		    else
 		    {
-			return !(e.arg(1) == concat(context->bv_val(0, 1), context->bv_val(-1, bvSize - 1)));
+			return e.arg(1) == concat(context->bv_val(0, 1), context->bv_val(-1, bvSize - 1));
 		    }
 		}
 		else
@@ -509,7 +510,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
 		    }
 		    else
 		    {
-			return !(e.arg(0) == concat(context->bv_val(1, 1), context->bv_val(0, bvSize - 1)));
+			return e.arg(0) == concat(context->bv_val(1, 1), context->bv_val(0, bvSize - 1));
 		    }
 		}
 		else
@@ -602,7 +603,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
 		    }
 		    else
 		    {
-			return !(e.arg(1) == context->bv_val(-1, bvSize));
+			return e.arg(1) == context->bv_val(-1, bvSize);
 		    }
 		}
 		else
@@ -631,7 +632,7 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
 		    }
 		    else
 		    {
-			return !(e.arg(0) == context->bv_val(0, bvSize));
+			return e.arg(0) == context->bv_val(0, bvSize);
 		    }
 		}
 		else