In C++ code, using solver.unsat_core() yields an empty result.

[ZechenWei]

Hello, I'm unable to get unsat_core() with the following SMT commands. No matter what, I only get an empty result. Normally, I should be able to get three results: a0, a1, and a2。 `

(set-option :produce-unsat-cores true) (declare-fun P$sn$1 () Bool) (declare-fun c$sn$1 () Real) (declare-fun b$sn$1 () Real) (declare-fun a$sn$1 () Real) (declare-fun v$sn$1 () Real) (declare-fun c$sn () Real) (declare-fun a1 () Bool) (declare-fun a2 () Bool) (declare-fun a0 () Bool) (assert (let (($x90 (and true P$sn$1))) (let (($x83 (> c$sn$1 0.0))) (let (($x80 (> b$sn$1 0.0))) (let (($x79 (> a$sn$1 0.0))) (let (($x81 (and $x79 $x80))) (let (($x82 (not $x81))) (let (($x84 (or $x82 $x83))) (let (($x85 (= P$sn$1 $x84))) (let (($x74 (> c$sn v$sn$1))) (let ((?x75 (ite $x74 c$sn v$sn$1))) (let (($x76 (= c$sn$1 ?x75))) (let (($x86 (and (and (and true (= v$sn$1 (+ a$sn$1 b$sn$1))) $x76) $x85))) (let (($x87 (=> $x86 $x90))) (not $x87))))))))))))))) (assert (let (($x83 (> c$sn$1 0.0))) (let (($x80 (> b$sn$1 0.0))) (let (($x79 (> a$sn$1 0.0))) (let (($x81 (and $x79 $x80))) (let (($x82 (not $x81))) (let (($x84 (or $x82 $x83))) (let (($x85 (= P$sn$1 $x84))) (let (($x97 (=> a1 $x85))) (let (($x74 (> c$sn v$sn$1))) (let ((?x75 (ite $x74 c$sn v$sn$1))) (let (($x76 (= c$sn$1 ?x75))) (let (($x96 (=> a2 $x76))) (let (($x126 (and (and true (=> a0 (= v$sn$1 (+ a$sn$1 b$sn$1)))) $x96))) (and $x126 $x97))))))))))))))) (check-sat-assuming (a0 a1 a2)) (get-unsat-core)

`

[NikolajBjorner]

remove the last constraint. It is already unsat. The core is therefore empty. It does not depend on any of the assumptions.