Z3/smt2_eval_Boolector inconsistency: QF_BV/log-slicing/bvashr_0250.smt2

[hriener]

This is not necessarily an issue of metaSMT.

[metaSMT] Instance is SAT
[z3] Instance is UNSAT

[hriener]

z3 is right; metaSMT is wrong.
QF_BV/log-slicing/bvashr_0250.smt2 smt2_eval_Boolector FAIL
QF_BV/log-slicing/bvashr_0273.smt2 smt2_eval_Boolector FAIL

[hriener]

BOOST_AUTO_TEST_CASE(Boolector_error)
{
  bitvector v923 = new_bitvector(250);
  bitvector v925 = new_bitvector(250);
  bitvector v934 = new_bitvector(256);
  bitvector v960 = new_bitvector(128);
  assertion( ctx, equal(v925, bvashr(v923, extract(249, 0, v934))) );
  assertion( ctx, equal(bvuint(0,6), extract(255,250,v934)) );
  assertion( ctx, equal(logic::False, equal(extract(127,64,bvand(v960,extract(255,128,v934))), bvuint(0,64))) );
  assertion( ctx, equal(extract(249,249,v923), bvuint(0,1)) );
  assertion( ctx, nequal(v925, bvuint(0,250)) );
  BOOST_REQUIRE( !solve(ctx) );
}

[hriener]

extern "C"{
#include <boolector.h>
}
#include <iostream>

int main( int argc, char* argv[] )
{
  Btor *btor = boolector_new();

  BoolectorNode* v923 = boolector_var( btor, 100, NULL );
  BoolectorNode* v934 = boolector_var( btor, 128, NULL );
  BoolectorNode* v960 = boolector_var( btor,  64, NULL );

  // assertion #1
  BoolectorNode* t0 = boolector_unsigned_int( btor, 253, 100 );
  BoolectorNode* t1 = boolector_slice( btor, v934, 99, 0 );
  BoolectorNode* t2 = boolector_sra( btor, v923, t1 );
  BoolectorNode* t3 = boolector_eq( btor, t2, t0 );
  boolector_assert( btor, t3 );

  // assertion #2
  BoolectorNode* t4 = boolector_unsigned_int( btor, 0, 28 );
  BoolectorNode* t5 = boolector_slice( btor, v934, 127, 100 );
  BoolectorNode* t6 = boolector_eq( btor, t4, t5 );
  boolector_assert( btor, t6 );

  // assertion #3
  BoolectorNode*  t7 = boolector_slice( btor, v934, 127, 64 );
  BoolectorNode*  t8 = boolector_and( btor, v960, t7 );
  BoolectorNode*  t9 = boolector_slice( btor, t8, 63, 32 );
  BoolectorNode* t10 = boolector_unsigned_int( btor, 0, 32 );
  BoolectorNode* t11 = boolector_ne( btor, t10, t9 );
  boolector_assert( btor, t11 );

  // assertion #4
  BoolectorNode* t12 = boolector_slice( btor, v923, 99, 99 );
  BoolectorNode* t13 = boolector_unsigned_int( btor, 0, 1 );
  BoolectorNode* t14 = boolector_eq( btor, t12, t13 );
  boolector_assert( btor, t14 );

  int result = boolector_sat (btor);
  if (result == BOOLECTOR_SAT)
  {
    std::cout << "SAT" << '\n';
  }
  else
  {
    std::cout << "UNSAT" << '\n';
  }

  // cleanup

  boolector_delete (btor);

  return 0;
}

[hriener]

(set-logic QF_BV)
(declare-fun v923 () (_ BitVec 100))
(declare-fun v934 () (_ BitVec 128))
(declare-fun v960 () (_ BitVec  64))

(declare-fun t0 () (_ BitVec 100))
(declare-fun t1 () (_ BitVec 100))
(declare-fun t2 () (_ BitVec 100))
(declare-fun t3 () Bool)
(assert (= t0 (_ bv253 100)) )
(assert (= t1 ((_ extract 99 0) v934)) )
(assert (= t2 (bvashr v923 t1)) )
(assert (= t3 (= t2 t0)) )
(assert t3)

(declare-fun t4 () (_ BitVec 28))
(declare-fun t5 () (_ BitVec 28))
(declare-fun t6 () Bool)
(assert (= t4 (_ bv0 28)) )
(assert (= t5 ((_ extract 127 100) v934)) )
(assert (= t6 (= t4 t5)) )
(assert t6)

(declare-fun t7 () (_ BitVec 64))
(declare-fun t8 () (_ BitVec 64))
(declare-fun t9 () (_ BitVec 32))
(declare-fun t10 () (_ BitVec 32))
(declare-fun t11 () Bool)
(assert (= t7 ((_ extract 127 64) v934)) )
(assert (= t8 (bvand v960 t7)) )
(assert (= t9 ((_ extract 63 32) t8)) )
(assert (= t10 (_ bv0 32)) )
(assert (= t11 (not (= t9 t10)) ) )
(assert t11)

(declare-fun t12 () (_ BitVec 1))
(declare-fun t13 () (_ BitVec 1))
(declare-fun t14 () Bool)
(assert (= t12 ((_ extract 99 99) v923)) )
(assert (= t13 (_ bv0 1)) )
(assert (= t14 (= t12 t13)) )
(assert t14)

(check-sat)

[hriener]

I reproduced the problem with Boolector boolector-1.5.118 and boolector-2.0.6 (installed from dependencies) with the native Boolector API. Thus, I conclude it's a Boolector-related issue; since boolector_sra does not support bit-widths unequal power of 2 it does not even make sense to file a bug. 😢