search

usi-verification-and-security / golem

Solver for Constrained Horn Clauses
MIT License
34 stars 7 forks source link

std::out_of_range when running with --print-witness #51

Closed rodrigo7491 closed 9 months ago

rodrigo7491 commented 9 months ago

When running chc-LIA_387 from CHC-COMP 2023, Golem outputs the following:

For the command golem chc-LIA_387.smt2 the output is sat.

For the command golem --print-witness chc-LIA_387.smt2 the output is as below.

sat
terminate called after throwing an instance of 'std::out_of_range'
  what():  basic_string::erase: __pos (which is 18446744073709551615) > this->size() (which is 6)
Aborted (core dumped)