stanford-centaur / smt-switch

A generic C++ API for SMT solving. It provides abstract classes which can be implemented by different SMT solvers.
Other
114 stars 43 forks source link

Calling `to_int` on a bitvector of size 1 causes a crash #308

Closed zyedidia closed 1 year ago

zyedidia commented 2 years ago

It seems like to_int assumes that the bitvector gets converted to a string of the form #bxxx, but for bitvectors of size 1 it is actually true or false (at least when using the bitwuzla solver). For example, the following code causes a crash in to_int:

SmtSolver solver = BitwuzlaSolverFactory::create(false);
solver->set_opt("produce-models", "true");
solver->set_opt("incremental", "true");

Sort sort = solver->make_sort(BV, 1);
Term x = solver->make_symbol("x", sort);
solver->check_sat();
uint64_t i = solver->get_value(x)->to_int();
std::cout << i << "\n";

I would instead expect to_int to return 0 or 1.

yoni206 commented 2 years ago

Thanks for posting the issue, I'll look into it.

yoni206 commented 2 years ago

We are having some issues with CI at the moment, but once #309 is merged, this issued should be fixed.