NullPointerException for NIA and ALIA formulas (unsat-core)

[rainoftime]

Hi, for the following formulas,

NPD.txt NPD2.txt

smtinterpol commit 0610d35 throws a NPD

[rainoftime]

At commit 7625fe26c, NPD.txt is fixed, while NPD2.txt is not

[tanjaschindler]

There seem to be problems with NamedAtom and check-sat-assuming.

[rainoftime]

Here is small case

(set-logic LRA)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const r1 Real)
(declare-const r3 Real)
(declare-const r4 Real)
(declare-const r6 Real)
(declare-const r8 Real)
(declare-const r11 Real)
(declare-const r13 Real)
(assert (! (xor v0 v1) :named IP_1))
(declare-const v3 Bool)
(declare-const r14 Real)
(declare-const r15 Real)
(assert (! (xor v2 (>= r1 0.79402645 r4 (- r13)) v1 (= 525.0 (- r13) 525.0 531735050.0 r4) v0 v1 v3 (= 525.0 (- r13) 525.0 531735050.0 r4) (= (xor v0 v1) v2 v1 v0 v1 v0 v0 (xor v0 v1) v1 (>= r1 0.79402645 r4 (- r13))) (>= r1 0.79402645 r4 (- r13)) v1) :named IP_2))
(assert (! v2 :named IP_3))
(check-sat)
(check-sat-assuming (IP_1 IP_3))