Task: Investigate memoization issues in computation on literals

[cpitclaudel]

In the abstract, I would expect the verification cost of the following methods to grow linearly:

function fib(n: nat): int {
  if n <= 1 then 1
  else fib(n - 1) + fib(n - 2)
}

method M0() { assert fib(00) == -1; }
method M1() { assert fib(10) == -1; }
method M2() { assert fib(20) == -1; }
method M3() { assert fib(30) == -1; }
method M4() { assert fib(40) == -1; }
method M5() { assert fib(50) == -1; }
method M6() { assert fib(60) == -1; }
method M7() { assert fib(70) == -1; }
method M8() { assert fib(80) == -1; }
method M9() { assert fib(90) == -1; }
method M10() { assert fib(100) == -1; }

This is because even though fib is written as an exponential function, calls to it "should" be memoized by the egraph.

But that's not what we're seeing:

Verifying Impl$$_module.__default.M0 ...
  [0.045 s, solver resource count: 61138, 2 proof obligations]  error
Verifying Impl$$_module.__default.M1 ...
  [0.038 s, solver resource count: 136757, 2 proof obligations]  error
Verifying Impl$$_module.__default.M2 ...
  [0.044 s, solver resource count: 369482, 2 proof obligations]  error
Verifying Impl$$_module.__default.M3 ...
  [0.062 s, solver resource count: 1114295, 2 proof obligations]  error
Verifying Impl$$_module.__default.M4 ...
  [0.109 s, solver resource count: 1830479, 2 proof obligations]  error
Verifying Impl$$_module.__default.M5 ...
  [0.492 s, solver resource count: 5187742, 2 proof obligations]  error
Verifying Impl$$_module.__default.M6 ...
  [0.622 s, solver resource count: 6556175, 2 proof obligations]  error
Verifying Impl$$_module.__default.M7 ...
  [1.325 s, solver resource count: 36901396, 2 proof obligations]  error
Verifying Impl$$_module.__default.M8 ...
  [1.332 s, solver resource count: 36901396, 2 proof obligations]  error
Verifying Impl$$_module.__default.M9 ...
  [1.358 s, solver resource count: 36901396, 2 proof obligations]  error
Verifying Impl$$_module.__default.M10 ...
  [1.398 s, solver resource count: 36901396, 2 proof obligations]  error