public static void solve3()

in src/main/java/workspace/HelloZ3.java [94:126]

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

	public static void solve3() {
		System.out.println("a < b + 5 and a % 10 = 0");

		Context ctx = new Context();

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

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

		BoolExpr c1 = ctx.mkLt(a, b_plus_five);
		//BoolExpr c2 = ctx.mkGt(a, ten);
		IntExpr c2 = ctx.mkMod(a, ten);
		BoolExpr c3 = ctx.mkEq(c2, zero);

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

		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();
	}