Deploying to gh-pages from @ 879a732 🚀

equivalence.html

@@ -215,18 +215,6 @@ <h1 id="hevm-equivalence"><a class="header" href="#hevm-equivalence"><code>hevm
                            Which heuristic should be used to determine if we are
                            in a loop: StackBased (default) or Naive
                            (default: StackBased)
-  --abstract-arithmetic    Use abstraction-refinement for complicated arithmetic
-                           functions such as MulMod. This runs the solver first
-                           with abstraction turned on, and if it returns a
-                           potential counterexample, the counterexample is
-                           refined to make sure it is a counterexample for the
-                           actual (not the abstracted) problem
-  --abstract-memory        Use abstraction-refinement for Memory. This runs the
-                           solver first with abstraction turned on, and if it
-                           returns a potential counterexample, the
-                           counterexample is refined to make sure it is a
-                           counterexample for the actual (not the abstracted)
-                           problem
 </code></pre>
 <p>Symbolically execute both the code given in <code>--code-a</code> and <code>--code-b</code> and try
 to prove equivalence between their outputs and storages. Extracting bytecode

print.html

@@ -1182,18 +1182,6 @@ <h2 id="using-forge-to-build-your-project-for-symbolic-execution"><a class="head
                            Which heuristic should be used to determine if we are
                            in a loop: StackBased (default) or Naive
                            (default: StackBased)
-  --abstract-arithmetic    Use abstraction-refinement for complicated arithmetic
-                           functions such as MulMod. This runs the solver first
-                           with abstraction turned on, and if it returns a
-                           potential counterexample, the counterexample is
-                           refined to make sure it is a counterexample for the
-                           actual (not the abstracted) problem
-  --abstract-memory        Use abstraction-refinement for Memory. This runs the
-                           solver first with abstraction turned on, and if it
-                           returns a potential counterexample, the
-                           counterexample is refined to make sure it is a
-                           counterexample for the actual (not the abstracted)
-                           problem
   --num-cex-fuzz INTEGER   Number of fuzzing tries to do to generate a
                            counterexample (default: 3) (default: 3)
   --ask-smt-iterations INTEGER
@@ -1366,18 +1354,6 @@ <h2 id="using-forge-to-build-your-project-for-symbolic-execution"><a class="head
                            Which heuristic should be used to determine if we are
                            in a loop: StackBased (default) or Naive
                            (default: StackBased)
-  --abstract-arithmetic    Use abstraction-refinement for complicated arithmetic
-                           functions such as MulMod. This runs the solver first
-                           with abstraction turned on, and if it returns a
-                           potential counterexample, the counterexample is
-                           refined to make sure it is a counterexample for the
-                           actual (not the abstracted) problem
-  --abstract-memory        Use abstraction-refinement for Memory. This runs the
-                           solver first with abstraction turned on, and if it
-                           returns a potential counterexample, the
-                           counterexample is refined to make sure it is a
-                           counterexample for the actual (not the abstracted)
-                           problem
 </code></pre>
 <p>Symbolically execute both the code given in <code>--code-a</code> and <code>--code-b</code> and try
 to prove equivalence between their outputs and storages. Extracting bytecode

test.html

@@ -215,18 +215,6 @@ <h1 id="hevm-test"><a class="header" href="#hevm-test"><code>hevm test</code></a
                            Which heuristic should be used to determine if we are
                            in a loop: StackBased (default) or Naive
                            (default: StackBased)
-  --abstract-arithmetic    Use abstraction-refinement for complicated arithmetic
-                           functions such as MulMod. This runs the solver first
-                           with abstraction turned on, and if it returns a
-                           potential counterexample, the counterexample is
-                           refined to make sure it is a counterexample for the
-                           actual (not the abstracted) problem
-  --abstract-memory        Use abstraction-refinement for Memory. This runs the
-                           solver first with abstraction turned on, and if it
-                           returns a potential counterexample, the
-                           counterexample is refined to make sure it is a
-                           counterexample for the actual (not the abstracted)
-                           problem
   --num-cex-fuzz INTEGER   Number of fuzzing tries to do to generate a
                            counterexample (default: 3) (default: 3)
   --ask-smt-iterations INTEGER