Skip to content

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

Open
@thomasspriggs

Description

@thomasspriggs

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

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions