diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2021-09-01 13:33:29 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2021-09-01 13:33:29 -0500 |
| commit | 6454b46ae4dd834c5ed1659639eedf7c4a88a2cb (patch) | |
| tree | 4b56a0310616746d2be44e348a0d756546bf397c | |
| parent | 1eae939aa065c648941a24151e0958d627a50ac8 (diff) | |
Format
| -rw-r--r-- | src/smt/proof_post_processor.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index f9d99c6a3..cf35eeb0c 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -1137,9 +1137,11 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, InferenceId iid; bool isRev; std::vector<Node> exp; - if (theory::strings::InferProofCons::unpackArgs(args, conc, iid, isRev, exp)) + if (theory::strings::InferProofCons::unpackArgs( + args, conc, iid, isRev, exp)) { - if (theory::strings::InferProofCons::addProofTo(cdp, conc, iid, isRev, exp)) + if (theory::strings::InferProofCons::addProofTo( + cdp, conc, iid, isRev, exp)) { return conc; } |