src/main/java/workspace/HelloZ3.java [80:91]:
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
		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();
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -



src/main/java/workspace/HelloZ3.java [114:125]:
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
		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();
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -