static void solve5()

in src/main/java/workspace/HelloZ3.java [156:187]

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

	static void solve5() {
		// a + 3 > 5

		Context ctx = new Context();
		Solver s = ctx.mkSolver();

		IntExpr a = ctx.mkIntConst("a");
		IntExpr five = ctx.mkInt(5);
		IntExpr three = ctx.mkInt(3);
		ArithExpr[] pluses = {a, three};
		ArithExpr a_plus_3 = ctx.mkAdd(pluses);

		BoolExpr a_bigger_five = ctx.mkLt(a_plus_3, five);

		System.out.println(a_bigger_five);
		//a_bigger_five = ctx.mkNot(a_bigger_five);
		s.add(a_bigger_five);
		if(s.check() == Status.SATISFIABLE) {
			System.out.println("SAT");
			Model model = s.getModel();
			System.out.println("a=" + model.evaluate(a, false));

			System.out.println(model.toString());
			//System.out.println(model.);
			//System.out.println(s.);

		} else {
			System.out.println("UNSAT");
		}


	}