Enabling unsat core generation makes solver result UNKNOWN on some inputs.

[MarcusVoelker]

public void testBug() {
    HashMap<String, String> options = new HashMap<>();
    options.put("proof", "true");
    options.put("model", "true");
    options.put("unsat_core", "true");
    Context context = new Context(options);
    Solver s = context.mkSolver();
    s.add(context.mkImplies(context.mkEq(context.mkIntConst("PC"), context.mkInt(0)), context.mkBoolConst("P0")));
    s.add(context.mkEq(context.mkBoolConst("P0"), context.mkLt(context.mkIntConst("Counter"), context.mkInt(17))));
    System.out.println(s.check());
}

Run the function, result is "UNKNOWN"
Removing the options.put("unsat_core", "true"); line makes the result, as expected, "SATISFIABLE".
Using the web interface at http://rise4fun.com/z3, I always get SATISFIABLE, even when using unsat core generation.

(set-option :produce-models true)
(set-option :produce-proofs true)
(set-option :produce-unsat-cores true)
(declare-fun PC () Int)
(declare-fun P0 () Bool)
(declare-fun Counter () Int)
(assert (=> (= PC 0) P0))
(assert (= P0 (< Counter 17)))
(check-sat)
(exit)

[NikolajBjorner]

Z3 doesn't really support simultaneous proof and core generation, but since your sample does not include core tracking I am bypassing the check. You can obtain the reason why a search returned unknown by querying ReasonUnknown/getReasonUnknown()/reason_unknown().