From 49e0b50183bcd195200d5230561c4e996821fdc7 Mon Sep 17 00:00:00 2001
From: Juan C <juanconrod@protonmail.com>
Date: Fri, 6 Oct 2023 19:33:08 +0200
Subject: [PATCH] Remove tweaks that are now part of Kontrol's default behavior

---
 test/FixedPointMathLib.k.sol |  5 -----
 test/run-kevm.sh             | 22 ++--------------------
 2 files changed, 2 insertions(+), 25 deletions(-)

diff --git a/test/FixedPointMathLib.k.sol b/test/FixedPointMathLib.k.sol
index e83f5d61..1e30f386 100644
--- a/test/FixedPointMathLib.k.sol
+++ b/test/FixedPointMathLib.k.sol
@@ -11,11 +11,6 @@ contract FixedPointMathLibVerification is Test, KevmUtil {
     // Constants
     uint256 constant WAD = 1e18;
 
-    function setUp() public {
-        // Make KEVM abstract gas computations
-        kevm.infiniteGas();
-    }
-
     function testMulWad(uint256 x, uint256 y) public {
 
         if(y == 0 || x <= type(uint256).max / y) {
diff --git a/test/run-kevm.sh b/test/run-kevm.sh
index ef81c47a..458e39a4 100755
--- a/test/run-kevm.sh
+++ b/test/run-kevm.sh
@@ -11,9 +11,7 @@ kontrol_kompile() {
             --verbose                 \
             --require ${lemmas}       \
             --module-import ${module} \
-            ${rekompile}              \
-            ${regen}                  \
-            ${llvm_library}
+            ${rekompile}
 }
 
 kontrol_prove() {
@@ -30,7 +28,6 @@ kontrol_prove() {
             ${implication_every_block}         \
             ${break_every_step}                \
             ${break_on_calls}                  \
-            ${auto_abstract}                   \
             ${tests}                           \
             ${use_booster}
 }
@@ -57,10 +54,6 @@ smt_timeout=100000
 workers=12
 
 # Switch the options below to turn them on or off
-# TODO: Describe this thoroughly
-regen=--regen
-#regen=
-
 rekompile=--rekompile
 #rekompile=
 
@@ -84,23 +77,12 @@ break_every_step=
 break_on_calls=
 break_on_calls=--no-break-on-calls
 
-auto_abstract=--auto-abstract
-auto_abstract=
-auto_abstract=--auto-abstract-gas
-
 bug_report=--bug-report
 bug_report=
 
 # For running the booster
-llvm_library=
-llvm_library=--with-llvm-library
-
-# For running the booster
-use_booster=
 use_booster=--use-booster
-
-kore_rpc_command=
-kore_rpc_command=kore-rpc-booster\ --simplify-after-exec\ --llvm-backend-library\ out/kompiled/llvm-library/interpreter.so
+#use_booster=
 
 # List of tests to symbolically execute