static void solve4()

in src/main/java/workspace/HelloZ3.java [128:154]

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

	static void solve4() {
		// a > 5

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

		IntExpr a = ctx.mkIntConst("a");
		IntExpr five = ctx.mkInt(5);
		BoolExpr a_bigger_five = ctx.mkLt(a, 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");
		}


	}