Z3/smt2_eval_STP inconsistency: QF_BV/sage/app7/bench_2935.smt2

[hriener]

This is not necessarily an issue of metaSMT.

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

[hriener]

BOOST_AUTO_TEST_CASE(STP_error)
{
  const unsigned w = 8u;
  bitvector v85 = new_bitvector( w );
  bitvector v88 = new_bitvector( w );
  assertion( ctx, equal( bvand( v88, bvuint(7,w) ), bvuint(3,w) ) );
  assertion( ctx, equal( bvand( v85, bvuint(7,w) ), bvuint(4,w) ) );
  assertion( ctx, bvsle( bvand( v88, bvuint(7,w)),
                         bvand( v85, bvuint(7,w)) ) );
  BOOST_REQUIRE( solve(ctx) );
}