summaryrefslogtreecommitdiff
path: root/src/theory/trust_substitutions.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-12-23 14:13:03 -0600
committerGitHub <noreply@github.com>2020-12-23 14:13:03 -0600
commit2594c961105110f6fce17983bfa69f68bd9ee15e (patch)
treea6c0b6fce46c3bd512c92b0c5643f1b34e4859c5 /src/theory/trust_substitutions.h
parent2937d0770d448e74b5cf9f9b02de31145a7c5738 (diff)
(proof-new) Miscelleneous fixes from proof-new (#5714)
Diffstat (limited to 'src/theory/trust_substitutions.h')
-rw-r--r--src/theory/trust_substitutions.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h
index 08e2da895..9b462c6da 100644
--- a/src/theory/trust_substitutions.h
+++ b/src/theory/trust_substitutions.h
@@ -40,7 +40,7 @@ class TrustSubstitutionMap
TrustSubstitutionMap(context::Context* c,
ProofNodeManager* pnm,
std::string name = "TrustSubstitutionMap",
- PfRule trustId = PfRule::TRUST_SUBS_MAP,
+ PfRule trustId = PfRule::PREPROCESS_LEMMA,
MethodId ids = MethodId::SB_DEFAULT);
/** Gets a reference to the underlying substitution map */
SubstitutionMap& get();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback