mcsat-assumptions branch: incorrect interpolant?

[disteph]

input file:

(set-option :produce-unsat-model-interpolants true)
(set-info :smt-lib-version 2.6)
(set-logic QF_BV)

(declare-fun x1()(_ BitVec 32))(declare-fun x2()(_ BitVec 32))(declare-fun x3()(_ BitVec 32))(declare-fun x4()(_ BitVec 32))(declare-fun y!0()(_ BitVec 32))(declare-fun y!1()(_ BitVec 32))(declare-fun y!2()(_ BitVec 32))(declare-fun y!3()(_ BitVec 32))(declare-fun forall_placeholder3()Bool)(declare-fun forall_placeholder2()Bool)(declare-fun forall_placeholder1()Bool)(declare-fun forall_placeholder0()Bool)(declare-fun y!4()(_ BitVec 32))(declare-fun y!5()(_ BitVec 32))(declare-fun y!6()(_ BitVec 32))(declare-fun y!7()(_ BitVec 32))(declare-fun forall_placeholder6()Bool)(declare-fun forall_placeholder5()Bool)(declare-fun forall_placeholder4()Bool)(declare-fun y!8()(_ BitVec 32))(declare-fun y!9()(_ BitVec 32))(declare-fun y!10()(_ BitVec 32))(declare-fun forall_placeholder8()Bool)(declare-fun forall_placeholder7()Bool)(declare-fun y!11()(_ BitVec 32))(declare-fun y!12()(_ BitVec 32))(declare-fun forall_placeholder9()Bool)(declare-fun y!13()(_ BitVec 32))

(assert(not(or(not(or(bvsge(bvadd(bvmul #b11111111111111111111111111110010 y!4)(bvmul #b00000000000000000000000000110001 y!8)(bvmul #b11111111111111111111111111000001 y!11)(bvmul #b00000000000000000000000001010111 y!13))#b00000000000000000000000001011110)(bvsge #b00000000000000000000000000001110(bvadd(bvmul #b00000000000000000000000001011000 y!4)(bvmul #b00000000000000000000000001010011 y!8)(bvmul #b11111111111111111111111111011101 y!13)))))(or(or(= #b11111111111111111111111111100001(bvadd(bvmul #b00000000000000000000000000011111 y!4)(bvmul #b11111111111111111111111110100000 y!8)(bvmul #b00000000000000000000000001000011 y!11)(bvmul #b11111111111111111111111111001001 y!13)))(not(= #b11111111111111111111111111101011(bvadd(bvmul #b00000000000000000000000001010001 y!4)(bvmul #b11111111111111111111111111101001 y!8)(bvmul #b11111111111111111111111111001010 y!13)))))(or(not(bvsge #b00000000000000000000000000000000(bvadd(bvmul #b00000000000000000000000001000101 y!4)(bvmul #b11111111111111111111111111111000 y!11))))(bvsge(bvadd(bvmul #b11111111111111111111111111001011 y!4)(bvmul #b11111111111111111111111111111100 y!11)(bvmul #b11111111111111111111111111011101 y!13))#b00000000000000000000000000011100))))))

(check-sat-assuming-model(forall_placeholder9 y!12 y!11 forall_placeholder7 forall_placeholder8 y!10 y!9 y!8 forall_placeholder4 forall_placeholder5 forall_placeholder6 y!7 y!6 y!5 y!4 forall_placeholder0 forall_placeholder1 forall_placeholder2 forall_placeholder3 y!3 y!2 y!1 y!0 x4 x3 x2 x1)(true #b00000000000000000000000000000000 #b01100001010010101001010000000101 true true #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b11111111111111111111111111111111 true false true #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b00000000000000000000000000000000 true false true true #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b00000000000000000000000000000000))

(get-unsat-model-interpolant)

(exit)

gives me interpolant

unsat
(or
 (bv-sge
  (bv-add (bv-mul 0b11111111111111111111111111110010 y!4) (bv-mul 0b00000000000000000000000000110001 y!8) (bv-mul 0b11111111111111111111111111000001 y!11)
          (bv-mul 0b00000000000000000000000001010111 y!13))
  0b00000000000000000000000001011110)
 (bv-sge
  0b00000000000000000000000000001110
  (bv-add (bv-mul 0b00000000000000000000000001011000 y!4) (bv-mul 0b00000000000000000000000001010011 y!8) (bv-mul 0b11111111111111111111111111011101 y!13))))

I can check via Yices' API that the "interpolant" evaluates to true in the model; my understanding is that it should evaluate to false. One can also check the evaluation by feeding the interpolant as a single assert, and then do check-sat-assuming-model, which should return unsat if the interpolant was correct. But I get sat, running on

(set-option :produce-unsat-model-interpolants true)
(set-info :smt-lib-version 2.6)
(set-logic QF_BV)

(declare-fun x1()(_ BitVec 32))(declare-fun x2()(_ BitVec 32))(declare-fun x3()(_ BitVec 32))(declare-fun x4()(_ BitVec 32))(declare-fun y!0()(_ BitVec 32))(declare-fun y!1()(_ BitVec 32))(declare-fun y!2()(_ BitVec 32))(declare-fun y!3()(_ BitVec 32))(declare-fun forall_placeholder3()Bool)(declare-fun forall_placeholder2()Bool)(declare-fun forall_placeholder1()Bool)(declare-fun forall_placeholder0()Bool)(declare-fun y!4()(_ BitVec 32))(declare-fun y!5()(_ BitVec 32))(declare-fun y!6()(_ BitVec 32))(declare-fun y!7()(_ BitVec 32))(declare-fun forall_placeholder6()Bool)(declare-fun forall_placeholder5()Bool)(declare-fun forall_placeholder4()Bool)(declare-fun y!8()(_ BitVec 32))(declare-fun y!9()(_ BitVec 32))(declare-fun y!10()(_ BitVec 32))(declare-fun forall_placeholder8()Bool)(declare-fun forall_placeholder7()Bool)(declare-fun y!11()(_ BitVec 32))(declare-fun y!12()(_ BitVec 32))(declare-fun forall_placeholder9()Bool)(declare-fun y!13()(_ BitVec 32))

(assert
(or
        (bvsge
                (bvadd (bvmul #b11111111111111111111111111110010 y!4) (bvmul #b00000000000000000000000000110001 y!8) (bvmul #b11111111111111111111111111000001 y!11)
                       (bvmul #b00000000000000000000000001010111 y!13))
                #b00000000000000000000000001011110)
        (bvsge
                #b00000000000000000000000000001110
                (bvadd(bvmul #b00000000000000000000000001011000 y!4)(bvmul #b00000000000000000000000001010011 y!8)(bvmul #b11111111111111111111111111011101 y!13)))))

(check-sat-assuming-model(forall_placeholder9 y!12 y!11 forall_placeholder7 forall_placeholder8 y!10 y!9 y!8 forall_placeholder4 forall_placeholder5 forall_placeholder6 y!7 y!6 y!5 y!4 forall_placeholder0 forall_placeholder1 forall_placeholder2 forall_placeholder3 y!3 y!2 y!1 y!0 x4 x3 x2 x1)(true #b00000000000000000000000000000000 #b01100001010010101001010000000101 true true #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b11111111111111111111111111111111 true false true #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b00000000000000000000000000000000 true false true true #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b00000000000000000000000000000000 #b00000000000000000000000000000000))

(get-unsat-model-interpolant)

(exit)

[dddejan]

I will take a look. It might take some time. In the meantime, if you have a way to make it the example smaller, that would be useful for debugging (e.g., no maybe try 2-bit bit-vectors, less variables, etc).

[disteph]

I'm trying out https://github.com/aniemetz/ddSMT to minimize the problem. But I get

function 'bvadd' expects (at least) 2 argument(s), 4 given

Indeed I give 4 arguments, but I thought that in SMTLib, bvadd could take more than 2. The doc says The operators in {bvand, bvor, bvadd, bvmul} have the :left-assoc attribute. at http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml.

Anyway, I can change my pretty-printer to use binary bvadd only... but I was just surprised.

[dddejan]

Not sure if SMTLIB is flexible, but ddSMT parse is such so probably better to do binary.

[BrunoDutertre]

Allowing n-ary bvadds is a relatively recent change. ddSMT was written before.

[disteph]

ah, thanks. I presume it's also the case of bvmul, etc. Anyway, even with binary bvadd, ddsmt chokes on (check-sat-assuming-model...) and (get-unsat-model-interpolant), understandably. Truncating the bitvector size from 32 to, say, 8, makes the problem disappear, so I'm running out of ideas to minimize the problem further. For what it's worth, running yices-mcsat in debug with --trace mcsat::bv::conflict::check doesn't complain, which tends to suggest that the theory lemmas are all correct...

[dddejan]

Actually I was suggesting to used ddSMT on the original quantified problem.

I assume that your solver will crash (or report error) because of this bug. You can just use ddSMT to make the original problem smaller while still crashing. I would be surprized if this doesn't work.

[disteph]

Yeah, I've just tried that. It reduced the file size a bit. Same interpolant, I think. The archive below gives:

• the quantified problem, reduced by ddsmt,
• the quantifier-free instance mimicking the API calls I make to the context that ends up producing the interpolant,
• an instance with the interpolant and the model, which should give unsat if the interpolant was good, but it gives sat. RND_3_21.dd.zip

[disteph]

Another similar one RND_4_11.dd.zip

[disteph]

Ah, this one is smaller: RND_3_4.dd.zip

[disteph]

Copying from Slack the simplified version of RND_3_4.dd, just to keep everything in one place:

(set-option :produce-unsat-model-interpolants true)
(set-logic QF_BV)
(declare-fun x () (_ BitVec 32))
(declare-fun y () (_ BitVec 32))
(assert 
  (= 
   #b00000000000000000000000000111001 
   (bvadd 
    (bvmul #b11111111111111111111111111010011 x) 
    (bvmul #b11111111111111111111111111111000 y))) 
  )
(assert 
 (or 
   (= 
    (bvmul #b00000000000000000000000000111101 x) 
    #b11111111111111111111111111101110)
   (bvsge 
    (bvmul #b00000000000000000000000001011011 x) 
    #b00000000000000000000000000111010)
   (not 
   (= 
    #b00000000000000000000000000111001 
    (bvadd 
     #b11010000000000000000000000000000 
     (bvmul #b11111111111111111111111111010011 x))))))
(check-sat-assuming-model 
 (y x) 
 (#b00000110000000000000000000000000 
  #b00000000000000000000000000000000))
(get-unsat-model-interpolant)

2 variables, 2 constraints. You force the values of the two variables, you get UNSAT, i.e., the conjunction of the two constraints evaluates to false. In fact, the first constraint evaluates to false, the second evaluates to true. But the interpolant you get is exactly the second constraint, though the interpolant should evaluate to false. If you remove the second constraint, or replacing it by "true", you get an interpolant that looks more meaningful.

[dddejan]

Attempt of fix committed. @disteph check it out and close if fixed.

[disteph]

It looks good, thanks!

[disteph]

I spoke too soon. It worked on the above example, and many others, but it still fails on another 53 instances. The smallest I find is this one:

(set-option :produce-unsat-model-interpolants true)
(set-logic QF_BV)
(declare-fun y!1 () (_ BitVec 8))
(declare-fun y!2 () (_ BitVec 8))
(declare-fun y!3 () (_ BitVec 8))
(declare-fun trig4 () Bool)
(assert 
 (or 
  (not 
   (or 
    (not 
      (= 
       #b00000001 
       y!1)) 
    (not 
      (= 
       #b00000000 
       y!2)) 
    (not 
     (= 
      (ite 
       (bvuge 
        y!1 
        #b01100100) 
       y!1 
       (bvadd y!1 y!2)) 
      y!3)))) 
  (not trig4)))
(check-sat-assuming-model 
 (trig4 y!3 y!2 y!1) 
 (true 
  #b00000000 
  #b00000000 
  #b00000000))
(get-unsat-model-interpolant)

It gives me unsat with the following interpolant

(or 
  (= 
   (ite 
    (bvuge 
     y!1 
     #b01100100) 
    y!1 
    (bvadd y!1 y!2)) 
   y!3) 
  (not trig4))

and the following file checks that the interpolant evaluates to true, not false:

(set-option :produce-unsat-model-interpolants true)
(set-logic QF_BV)
(declare-fun y!1 () (_ BitVec 8))
(declare-fun y!2 () (_ BitVec 8))
(declare-fun y!3 () (_ BitVec 8))
(declare-fun trig4 () Bool)
(assert 
 (or 
  (= 
   (ite 
    (bvuge 
     y!1 
     #b01100100) 
    y!1 
    (bvadd y!1 y!2)) 
   y!3) 
  (not trig4)))
(check-sat-assuming-model 
 (trig4 y!3 y!2 y!1) 
 (true 
  #b00000000 
  #b00000000 
  #b00000000))

[dddejan]

Ok, yet another fix added. @disteph another round.

Btw, if you run it with --trace mcsat::interpolant::check it will check the resulting interpolant.

[disteph]

Looks good now, thanks!