summaryrefslogtreecommitdiff
path: root/src/preprocessing
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing')
-rw-r--r--src/preprocessing/passes/ackermann.cpp4
-rw-r--r--src/preprocessing/passes/ackermann.h4
2 files changed, 3 insertions, 5 deletions
diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index 4b5873e80..87c7fa2ce 100644
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -35,8 +35,7 @@ namespace passes {
/* -------------------------------------------------------------------------- */
-namespace
-{
+namespace {
void addLemmaForPair(TNode args1,
TNode args2,
@@ -219,7 +218,6 @@ PreprocessingPassResult Ackermann::applyInternal(
return PreprocessingPassResult::NO_CONFLICT;
}
-
/* -------------------------------------------------------------------------- */
} // namespace passes
diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h
index 8f27cab25..410dde8b9 100644
--- a/src/preprocessing/passes/ackermann.h
+++ b/src/preprocessing/passes/ackermann.h
@@ -55,8 +55,8 @@ class Ackermann : public PreprocessingPass
* occurring in the input formula, add the following lemma:
* (x_1 = y_1 /\ ... /\ x_n = y_n) => f_X = f_Y
*/
- PreprocessingPassResult applyInternal(
- AssertionPipeline* assertionsToPreprocess) override;
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
private:
/* Map each function to a set of terms associated with it */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback