Invalid interpolants in MathSAT

[daniel-raffler]

Hello,

We've noticed, that some of the interpolants returned by MathSAT don't seem to be part of a valid interpolation sequence. Examples for this can be found when running imc in CPAchecker with cpa.predicate.refinement.verifyInterpolants set to true. Here are some benchmark results with a 60s time limit. The runs with invalid interpolants can be set by setting the filter to Exception. The problem doesn't appear to be very common, but there are roughly twice as many instances when calculating the interpolants backwards. The full benchmark set with error logs can be found here

I was able to extract a SMTLIB example to trigger the bug from one of the runs:

(set-option :produce-interpolants true)

(declare-const a (_ BitVec 8))
(declare-const b (_ BitVec 1))
(declare-const c (_ BitVec 2))
(declare-const d (_ BitVec 1))
(declare-const e (_ BitVec 32))

(assert (! (and (= e ((_ sign_extend 24) ((_ zero_extend 7) d))) (= ((_ zero_extend 6) c) ((_ extract 7 0) e))) :interpolation-group A))
(assert (! (= e ((_ sign_extend 24) a)) :interpolation-group B))
(assert (! (and (= ((_ sign_extend 24) a) ((_ sign_extend 24) ((_ zero_extend 7) b))) (not (= ((_ sign_extend 24) ((_ zero_extend 7) b)) ((_ sign_extend 24) ((_ zero_extend 6) c))))) :interpolation-group C))

(check-sat)

(echo "I1:")
(get-interpolant (A))

(echo "I2:")
(get-interpolant (A B))

MathSAT will return the following two interpolants:

daniel@notebook:~/workspace/mathsat-5.6.17-linux-x86_64/bin$ ./mathsat -proof_generation=true -theory.bv.eager=false ~/workspace/mathsat.mini.smt2 
unsat
"I1:"
(and (not (bvult (_ bv1 32) (bvadd ((_ zero_extend 30) c) (bvmul (_ bv4294967040 32) (bvlshr (bvadd (bvmul (_ bv4294967295 32) e) ((_ zero_extend 30) c)) (_ bv8 32)))))) (not (bvult e ((_ zero_extend 30) c))))
"I2:"
(let ((.def_110 ((_ extract 0 0) a))) (let ((.def_111 ((_ extract 0 0) c))) (and (and (= (bvand .def_110 (bvnot .def_111)) (_ bv0 1)) (= (bvand .def_111 (bvnot .def_110)) (_ bv0 1))) (= ((_ extract 1 1) c) (_ bv0 1)))))

Since I1 & B -> I2 does not hold, this is not a valid interpolation sequence

(Note, that MathSAT extracts its interpolants from the same proof. So, interpolants should always be part of a sequence, even when they are queried separately)

[baierd]

Thank you very much for investigating!

2 things we should check before reporting these:

• did we re-build the context in CPAchecker before generating these?
• was there a caught and accepted solver based exception before these were generated?

[daniel-raffler]

Hello Daniel

Thank you very much for investigating!

2 things we should check before reporting these:

* did we re-build the context in CPAchecker before generating these?

* was there a caught and accepted solver based exception before these were generated?

When I debugged this a few days ago, there were some cases when the invalid interpolant was returned after a caught exception, and after the prover stack had been rebuilt. However, that wasn't the case for all of the runs, and sometimes MathSAT would return invalid interpolants without any SolverException before that

Note, that for the results in this thread I used cpa.predicate.refinement.strategy=SEQ, which means that we don't try to rebuild the prover when there is a SolverException. Since the problem can also be reproduced with just SMTLIB, I don't think it's related to any of our error handling logic