Support for the internal push/pop interface is unimplemented in incremental smt2 decision procedure
Opened this issue · 0 comments
thomasspriggs commented
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