Fixes.

UnconstrainedVariableSimplifier.cpp

@@ -485,7 +485,15 @@ 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));
+		    auto result = e.arg(1) == concat(context->bv_val(0, 1), context->bv_val(-1, bvSize - 1));
+		    if (isPositive)
+		    {
+			return result;
+		    }
+		    else
+		    {
+			return !result;
+		    }
 		}
 	    }
 	    else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1)))
@@ -506,7 +514,15 @@ 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));
+		    auto result = e.arg(0) == concat(context->bv_val(1, 1), context->bv_val(0, bvSize - 1));
+		    if (isPositive)
+		    {
+			return result;
+		    }
+		    else
+		    {
+			return !result;
+		    }
 		}
 	    }
 	}
@@ -530,7 +546,15 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
 		}
 		else
 		{
-		    return context->bool_val(false);
+		    auto result = context->bool_val(false);
+		    if (isPositive)
+		    {
+			return result;
+		    }
+		    else
+		    {
+			return !result;
+		    }
 		}
 	    }
 	    else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1)))
@@ -551,7 +575,15 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
 		}
 		else
 		{
-		    return context->bool_val(false);
+		    auto result = context->bool_val(false);
+		    if (isPositive)
+		    {
+			return result;
+		    }
+		    else
+		    {
+			return !result;
+		    }
 		}
 	    }
 	}
@@ -575,7 +607,15 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
 		}
 		else
 		{
-		    return e.arg(1) == context->bv_val(-1, bvSize);
+		    auto result = e.arg(1) == context->bv_val(-1, bvSize);
+		    if (isPositive)
+		    {
+			return result;
+		    }
+		    else
+		    {
+			return !result;
+		    }
 		}
 	    }
 	    else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1)))
@@ -596,7 +636,15 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
 		}
 		else
 		{
-		    return e.arg(0) == context->bv_val(0, bvSize);
+		    auto result = e.arg(0) == context->bv_val(0, bvSize);
+		    if (isPositive)
+		    {
+			return result;
+		    }
+		    else
+		    {
+			return !result;
+		    }
 		}
 	    }
 	}
@@ -620,7 +668,15 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
 		}
 		else
 		{
-		    return context->bool_val(false);
+		    auto result = context->bool_val(false);
+		    if (isPositive)
+		    {
+			return result;
+		    }
+		    else
+		    {
+			return !result;
+		    }
 		}
 	    }
 	    else if (isUnconstrained(e.arg(1), boundVars) && isBefore(e.arg(0), e.arg(1)))
@@ -641,7 +697,15 @@ z3::expr UnconstrainedVariableSimplifier::simplifyOnce(expr e, std::vector<Bound
 		}
 		else
 		{
-		    return context->bool_val(false);
+		    auto result = context->bool_val(false);
+		    if (isPositive)
+		    {
+			return result;
+		    }
+		    else
+		    {
+			return !result;
+		    }
 		}
 	    }
 	}

main.cpp

@@ -23,16 +23,17 @@ int main(int argc, char* argv[])
 	{"count-locally", no_argument, 0, 'l' },
 	{"canonize", no_argument, 0, 'c' },
 	{"run-z3", no_argument, 0, 'z' },
+	{"inprocess", no_argument, 0, 'i' },
 	{0,           0,                 0,  0   }
     };
 
-    bool propagateUnconstrainedFlag = false, runZ3 = false, canonize = false, countVariablesLocally = false;
+    bool propagateUnconstrainedFlag = false, runZ3 = false, canonize = false, countVariablesLocally = false, inprocess = false;
     char* filename;
 
     int opt = 0;
 
     int long_index = 0;
-    while ((opt = getopt_long(argc, argv,"plzc", long_options, &long_index )) != -1)
+    while ((opt = getopt_long(argc, argv,"plzci", long_options, &long_index )) != -1)
     {
 	switch (opt)
 	{
@@ -45,6 +46,9 @@ int main(int argc, char* argv[])
 	case 'z':
 	    runZ3 = true;
 	    break;
+	case 'i':
+	    inprocess = true;
+	    break;
 	case 'c':
 	    canonize = true;
 	    break;
@@ -78,11 +82,35 @@ int main(int argc, char* argv[])
 
     if (propagateUnconstrainedFlag)
     {
-	UnconstrainedVariableSimplifier simplifier(ctx, e);
-	simplifier.SetCountVariablesLocally(countVariablesLocally);
-	//simplifier.PrintUnconstrained();
-	simplifier.SimplifyIte();
-	e = simplifier.GetExpr();
+	unsigned oldHash = 0;
+
+	do
+	{
+	    oldHash = e.hash();
+	    UnconstrainedVariableSimplifier simplifier(ctx, e);
+	    simplifier.SetCountVariablesLocally(countVariablesLocally);
+	    //simplifier.PrintUnconstrained();
+	    simplifier.SimplifyIte();
+	    e = simplifier.GetExpr();
+
+	    if (inprocess)
+	    {
+		z3::goal g(ctx);
+		g.add(e);
+
+		z3::tactic derTactic =
+		    z3::tactic(ctx, "simplify") &
+		    z3::tactic(ctx, "elim-and") &
+		    z3::tactic(ctx, "der") &
+		    z3::tactic(ctx, "simplify");
+
+		z3::apply_result result = derTactic(g);
+
+		assert(result.size() == 1);
+		z3::goal simplified = result[0];
+		e = simplified.as_expr();
+	    }
+	} while (oldHash != e.hash());
     }
 
     e = e.simplify();
@@ -90,11 +118,13 @@ int main(int argc, char* argv[])
 
     if (runZ3)
     {
-	solver s(ctx);
-	s.add(e);
+        solver s(ctx);
 	params p(ctx);
-	p.set("smt.timeout", 5000u);
+
+	//	p.set(":max_memory", 3u);
 	s.set(p);
+
+	s.add(e);
 	std::cout << s.check() << std::endl;
     }
     else