3#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H
4#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H
10 const irept &parse_tree,
11 const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table);
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
There are a large number of kinds of tree structured or tree-like data in CPROVER.
response_or_errort< smt_responset > validate_smt_response(const irept &parse_tree, const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table)