static void solve()

in src/main/java/workspace/HelloZ3.java [41:60]

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

	static void solve() {
		Context ctx = new Context();
		Solver s = ctx.mkSolver();

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

		s.add(ctx.mkLt( a,  five));

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

		ctx.close();

	}