Bizarre output for the get-value command

[LeventErkok]

For this benchmark:

(set-option :produce-models true)
(set-logic QF_UFBV)
(declare-fun s0 () (_ BitVec 8))
(declare-fun s1 () (_ BitVec 8))
(declare-fun s2 () (_ BitVec 8))
(declare-fun table0 ((_ BitVec 8)) (_ BitVec 8))
(define-fun s4 () (_ BitVec 8) (ite (bvule #x02 s2) #x00 (table0 s2)))
(define-fun s6 () Bool (= s4 #x02))
(assert (= (table0 #x00) s0))
(assert (= (table0 #x01) s1))
(assert (not s6))
(check-sat)
(get-value (s0))
(get-value (s1))

I get:

$ yices-smt2 b.smt2
sat
((s0 #b00000000))
((s1 ???))

Not quite sure what to make of the (s1 ???) output there on the last line.

I'm not on the bleeding edge, but the build is fairly new:

$ yices-smt2 --version
Yices 2.6.0
Copyright SRI International.
Linked with GMP 6.1.2
Copyright Free Software Foundation, Inc.
Build date: 2018-07-11
Platform: x86_64-apple-darwin17.7.0 (release)

[BrunoDutertre]

This means that Yices doesn't have a value for s1 in the model. I'll check why this happens in this case.

[BrunoDutertre]

@LeventErkok: A simple work-around is to change the logic to QF_ABV instead of QF_UFBV.

In your example, variable s1 is eliminated. When you ask for its value, Yices tries to compute the value of (table0 #x01) which is not defined. The reason is that the egraph builds only a partial model for table. To get a full model, you have to make sure that the array solver is used. That's why QF_ABV works here.

I'll see if we can fix the egraph to generate a full model.