@@ -0,0 +1,1213 @@
+package de.bmoth.backend.translator;%0A%0Aimport static org.junit.Assert.assertEquals;%0A%0Aimport org.junit.After;%0Aimport org.junit.Before;%0Aimport org.junit.Test;%0A%0Aimport com.microsoft.z3.BoolExpr;%0Aimport com.microsoft.z3.IntExpr;%0Aimport com.microsoft.z3.InterpolationContext;%0Aimport com.microsoft.z3.InterpolationContext.ComputeInterpolantResult;%0Aimport com.microsoft.z3.Solver;%0Aimport com.microsoft.z3.Status;%0A%0Apublic class Z3InterpolationTest %7B%0A%09private InterpolationContext ctx;%0A%09private Solver s;%0A%0A%09@Before%0A%09public void setup() %7B%0A%09%09ctx = InterpolationContext.mkContext();%0A%09%09s = ctx.mkSolver();%0A%09%7D%0A%0A%09@After%0A%09public void cleanup() %7B%0A%09%09ctx.close();%0A%09%7D%0A%0A%09@Test%0A%09public void testSimpleInterpolation() %7B%0A%09%09IntExpr x = ctx.mkIntConst(%22x%22);%0A%09%09BoolExpr xGtZero = ctx.mkGt(x, ctx.mkInt(0));%0A%09%09BoolExpr xLtZero = ctx.mkLt(x, ctx.mkInt(0));%0A%0A%09%09BoolExpr xGtZeroInterpolant = ctx.MkInterpolant(xGtZero);%0A%0A%09%09s.add(xGtZero);%0A%09%09s.add(xLtZero);%0A%0A%09%09Status check = s.check();%0A%09%09assertEquals(Status.UNSATISFIABLE, check);%0A%0A%09%09ComputeInterpolantResult ir = ctx.ComputeInterpolant(ctx.mkAnd(xGtZeroInterpolant, xLtZero), ctx.mkParams());%0A%09%09assertEquals(1, ir.interp.length);%0A%09%09assertEquals(%22(not (%3C= x 0))%22, ir.interp%5B0%5D.toString());%0A%09%7D%0A%7D%0A

add test case for interpolation