chore: add more sources

opencompl · Sep 28, 2024 · a265977 · a265977
1 parent 04e1661
commit a265977
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/Lean/Elab/Tactic/BVAckermannize.lean b/src/Lean/Elab/Tactic/BVAckermannize.lean
@@ -7,6 +7,8 @@ This file implements lazy ackermannization [1, 2]
 
 [1] https://lara.epfl.ch/w/_media/model-based.pdf
 [2]  https://leodemoura.github.io/files/oregon08.pdf
+[3] https://github.com/Z3Prover/z3/blob/d047b86439ec209446d211f0f6b251ebfba070d8/src/ackermannization/lackr.cpp#L206
+[4]https://github.com/Z3Prover/z3/blob/d047b86439ec209446d211f0f6b251ebfba070d8/src/ackermannization/lackr_model_constructor.cpp#L344
 -/
 prelude
 import Std.Tactic.BVDecide.Bitblast