boolector_bv_assignment output doesn't match docs

[cdisselkoen]

Changing the setting BTOR_OPT_OUTPUT_NUMBER_FORMAT to be BTOR_OUTPUT_BASE_HEX appears to enable hexadecimal output not only in dumps, but also in the return value of boolector_bv_assignment(), contradicting the boolector_bv_assignment docs which say that "Each character of the string can be 0, 1 or x". I'm not sure whether this is a documentation bug, and BTOR_OPT_OUTPUT_NUMBER_FORMAT is indeed meant to apply here - in which case, will the character be x if any of the 4 bits it represents are x? - or if this is an actual functionality bug, and BTOR_OPT_OUTPUT_NUMBER_FORMAT is not meant to affect the output of boolector_bv_assignment().

I get this behavior both with Boolector commit fa434d30 and with commit fafab47e. (Respectively, those are latest-master-at-time-of-writing, and the git tag 3.1.0.)

[cdisselkoen]

Code example:

#include <boolector.h>
#include <btoropt.h>
#include <stdio.h>
#include <stdlib.h>

int main(int argc, char* argv[]) {
  Btor* btor = boolector_new();
  boolector_set_opt(btor, BTOR_OPT_OUTPUT_NUMBER_FORMAT, BTOR_OUTPUT_BASE_HEX);
  boolector_set_opt(btor, BTOR_OPT_MODEL_GEN, 2);

  BoolectorSort sort = boolector_bitvec_sort(btor, 32);
  BoolectorNode* constant = boolector_consth(btor, sort, "a1face");
  BoolectorNode* bv = boolector_var(btor, sort, "bv");
  boolector_assert(btor, boolector_eq(btor, bv, constant));

  assert(boolector_sat(btor) == BOOLECTOR_SAT);

  printf("%s\n", boolector_bv_assignment(btor, bv));

  return 0;
}

[aniemetz]

Good catch! That's actually a documentation bug. Fixed in https://github.com/Boolector/boolector/commit/510eb28655ca14c637c7e11e73a1cf56d0b744a8.