diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2021-09-01 08:28:39 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2021-09-01 08:28:39 -0500 |
| commit | f77fa45cb56c4156e5610ebd2a8ac0e791583937 (patch) | |
| tree | 1691252be8cc8ef744465b465bad1abdd8447a08 | |
| parent | aee791fc94e6455450b5b56867d6b661270f6dba (diff) | |
Fix namespace
| -rw-r--r-- | src/smt/proof_post_processor.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 98fcc4f78..f9d99c6a3 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -1137,9 +1137,9 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, InferenceId iid; bool isRev; std::vector<Node> exp; - if (strings::InferProofCons::unpackArgs(args, conc, iid, isRev, exp)) + if (theory::strings::InferProofCons::unpackArgs(args, conc, iid, isRev, exp)) { - if (strings::InferProofCons::addProofTo(cdp, conc, iid, isRev, exp)) + if (theory::strings::InferProofCons::addProofTo(cdp, conc, iid, isRev, exp)) { return conc; } |