When using the Solver's from_string method in z3py to load a SMT2 file, unsat cores are produced correctly for tracked assertions in the smtlib file. However, if I switch from using Solver to Optimize, the unsat core list is always empty.

Also - to produce unsat cores with a Solver when using from_string, I have to include (set-option :produce-unsat-cores true) in the smtlib file as solver.set(unsat_core=True) doesn't seem to affect the from_string call. I'm not sure whether this is expected behavior or not.