public static void solve2()

in src/main/java/workspace/HelloZ3.java [63:92]

• 23 lines of code
• 2 McCabe index (conditional complexity)

    public static void solve2() {
		System.out.println("a < b + 5, 10 > a");

		Context ctx = new Context();

		IntExpr a = ctx.mkIntConst("a");
		IntExpr b = ctx.mkIntConst("b");
		IntExpr five = ctx.mkInt(5);
		IntExpr ten = ctx.mkInt(10);

		ArithExpr b_plus_five = ctx.mkAdd(b, five);

		BoolExpr c1 = ctx.mkLt(a, b_plus_five);
		BoolExpr c2 = ctx.mkGt(a, ten);

		BoolExpr q = ctx.mkAnd(c1, c2);

		Solver s = ctx.mkSolver();
		s.add(q);
		if(s.check() == Status.SATISFIABLE) {
			System.out.println("SAT");
			Model model = s.getModel();
			System.out.println("a=" + model.evaluate(a, false) +
					"b=" + model.evaluate(b, false));
		} else {
			System.out.println("UNSAT");
		}

		ctx.close();
	}