summaryrefslogtreecommitdiff
path: root/src/proof/proof_utils.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/proof_utils.h')
-rw-r--r--src/proof/proof_utils.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h
index b172217d8..a7590451d 100644
--- a/src/proof/proof_utils.h
+++ b/src/proof/proof_utils.h
@@ -88,6 +88,7 @@ typedef std::vector<LetOrderElement> Bindings;
namespace utils {
std::string toLFSCKind(Kind kind);
+std::string toLFSCKindTerm(Expr node);
inline unsigned getExtractHigh(Expr node) {
return node.getOperator().getConst<BitVectorExtract>().high;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback