diffblue/cbmc

Support for the internal push/pop interface is unimplemented in incremental smt2 decision procedure

Opened this issue · 0 comments

Support for the internal push/pop interface is unimplemented in incremental smt2 decision procedure. The lack of support causes the error message - Invariant failed: push. This internal interface is the following functions -

void smt2_incremental_decision_proceduret::push(
  const std::vector<exprt> &assumptions);
void smt2_incremental_decision_proceduret::push();
void smt2_incremental_decision_proceduret::pop();

These should be relatively trivial to implement as the push/pop commands and their printing already exists in the AST.

This unimplemented feature is known to affect support for the --localize-fault argument. This affects the following test - cbmc/fault_localization-stop_on_fail1/test.desc