Turn off aux lemmas by default

runtimeverification · Aug 21, 2024 · 55b3991 · 55b3991
1 parent d6599f0
commit 55b3991
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 6 deletions.
diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py
@@ -351,11 +351,11 @@ def parse(s: str) -> list[T]:
         help='Do not include assumptions on keccak properties.',
     )
     build.add_argument(
-        '--no-auxiliary-lemmas',
+        '--auxiliary-lemmas',
         dest='auxiliary_lemmas',
         default=None,
-        action='store_false',
-        help='Do not include auxiliary Kontrol lemmas.',
+        action='store_true',
+        help='Include auxiliary Kontrol lemmas.',
     )
 
     state_diff_args = command_parser.add_parser(

diff --git a/src/kontrol/options.py b/src/kontrol/options.py
@@ -833,7 +833,7 @@ def default() -> dict[str, Any]:
             'no_silence_warnings': False,
             'no_metadata': False,
             'keccak_lemmas': True,
-            'auxiliary_lemmas': True,
+            'auxiliary_lemmas': False,
         }
 
     @staticmethod

diff --git a/src/tests/integration/test-data/show/foundry.k.expected b/src/tests/integration/test-data/show/foundry.k.expected
@@ -4,7 +4,6 @@ requires "requires/cse-lemmas.k"
 requires "requires/pausability-lemmas.k"
 requires "requires/symbolic-bytes-lemmas.k"
 requires "requires/keccak.md"
-requires "requires/kontrol_lemmas.md"
 
 module FOUNDRY-MAIN
     imports public S2KsrcZModduplicatesZMod2ZModDuplicateName-VERIFICATION
@@ -163,7 +162,6 @@ module FOUNDRY-MAIN
     imports public S2KlibZModforgeZSubstdZModsrcZModsafeconsole-VERIFICATION
     imports public S2KlibZModforgeZSubstdZModlibZModdsZSubtestZModsrcZModDSTest-VERIFICATION
     imports public KECCAK-LEMMAS
-    imports public KONTROL-AUX-LEMMAS