Certora QF_UFBV benchmarks

SMT-LIB · Nov 13, 2024 · ecc1705 · ecc1705
1 parent 02e00a1
commit ecc1705
Show file tree

Hide file tree

Showing 1,029 changed files with 1,231,853 additions and 0 deletions.
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0000.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0000.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0003.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0003.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0010.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0010.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0011.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0011.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0012.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0012.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0013.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0013.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0016.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0016.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0019.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0019.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0021.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0021.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0022.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0022.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0023.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0023.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0028.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0028.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0030.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0030.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0031.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0031.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0032.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0032.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0034.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0034.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0035.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0035.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0036.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0036.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0037.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0037.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0039.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0039.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0054.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0054.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0057.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0057.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0062.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0062.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0066.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0066.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0069.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0069.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0072.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0072.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0080.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0080.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0090.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0090.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0103.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0103.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0104.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0104.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0108.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0108.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0109.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0109.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0111.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0111.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0112.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0112.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0113.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0113.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0114.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0114.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0116.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0116.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0117.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0117.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0125.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0125.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0132.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0132.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0136.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0136.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0146.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0146.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0147.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0147.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0150.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0150.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0153.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0153.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0158.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0158.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0160.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0160.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0162.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0162.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0165.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0165.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0166.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0166.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0170.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0170.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0172.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0172.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0179.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0179.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0180.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0180.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0181.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0181.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0182.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0182.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0184.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0184.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0188.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0188.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0190.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0190.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0191.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0191.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0192.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0192.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0198.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0198.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0205.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0205.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0208.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0208.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0212.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0212.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0231.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0231.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0234.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0234.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0240.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0240.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0242.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0242.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0247.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0247.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0249.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0249.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0251.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0251.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0253.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0253.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0261.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0261.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0262.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0262.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0278.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0278.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0280.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0280.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0282.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0282.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0283.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0283.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0285.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0285.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0286.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0286.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0287.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0287.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0288.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0288.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0294.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0294.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0302.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0302.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0309.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0309.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0318.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0318.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0319.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0319.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0321.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0321.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0323.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0323.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0328.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0328.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0330.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0330.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0331.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0331.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0337.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0337.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0338.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0338.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0341.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0341.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0343.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0343.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0350.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0350.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0351.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0351.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0352.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0352.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0354.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0354.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0355.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0355.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0359.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0359.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0360.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0360.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0361.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0361.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0363.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0363.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0369.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0369.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0371.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0371.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0374.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0374.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0382.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0382.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0387.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0387.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0390.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0390.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0394.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0394.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0395.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0395.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0398.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0398.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0399.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0399.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0403.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0403.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0406.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0406.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0407.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0407.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0408.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0408.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0412.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0412.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0413.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0413.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0415.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0415.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0418.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0418.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0419.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0419.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0421.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0421.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0422.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0422.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0423.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0423.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0425.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0425.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0426.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0426.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0433.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0433.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0435.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0435.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0437.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0437.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0444.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0444.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0445.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0445.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0446.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0446.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0447.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0447.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0448.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0448.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0449.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0449.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0456.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0456.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0457.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0457.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0458.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0458.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0459.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0459.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0460.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0460.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0461.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0461.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0495.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0495.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0497.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0497.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0498.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0498.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0499.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0499.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0618.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0618.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0648.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0648.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0649.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0649.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0650.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0650.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0651.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0651.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0652.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0652.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0653.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0653.smt2
diff --git a/non-incremental/QF_UFBV/20241113-Certora/0654.smt2 b/non-incremental/QF_UFBV/20241113-Certora/0654.smt2
@@ -0,0 +1,137 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_UFBV)
+(set-info :source |
+Generated by: Certora
+Generated on: 2024-01-16
+Generator: The Certora Prover
+Application: Web3 security
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+(declare-fun x15 () (_ BitVec 256))
+(declare-fun x71 () (_ BitVec 256))
+(declare-fun x10 () (_ BitVec 256))
+(declare-fun x58 () (_ BitVec 256))
+(declare-fun x3 () (_ BitVec 256))
+(declare-fun x68 () (_ BitVec 256))
+(declare-fun x41 () (_ BitVec 256))
+(declare-fun x42 () (_ BitVec 256))
+(declare-fun x75 ((_ BitVec 256)) (_ BitVec 256))
+(declare-fun x73 () (_ BitVec 256))
+(declare-fun x9 () (_ BitVec 256))
+(declare-fun x77 ((_ BitVec 256)) (_ BitVec 256))
+(declare-fun x70 () (_ BitVec 256))
+(declare-fun x84 () (_ BitVec 256))
+(declare-fun x65 () (_ BitVec 256))
+(declare-fun x62 () (_ BitVec 256))
+(declare-fun x61 ((_ BitVec 256)) (_ BitVec 256))
+(declare-fun x27 () (_ BitVec 256))
+(declare-fun x48 ((_ BitVec 256)) (_ BitVec 256))
+(declare-fun x11 () (_ BitVec 256))
+(declare-fun x63 () (_ BitVec 256))
+(declare-fun x25 () (_ BitVec 256))
+(declare-fun x74 () (_ BitVec 256))
+(declare-fun x5 () Bool)
+(declare-fun x66 () (_ BitVec 256))
+(declare-fun x21 ((_ BitVec 256)) (_ BitVec 256))
+(declare-fun x45 ((_ BitVec 256)) Bool)
+(declare-fun x64 () (_ BitVec 256))
+(declare-fun x35 () Bool)
+(declare-fun x7 () (_ BitVec 256))
+(declare-fun x56 () (_ BitVec 256))
+(declare-fun x2 () (_ BitVec 256))
+(declare-fun x4 () Bool)
+(declare-fun x54 () (_ BitVec 256))
+(declare-fun x22 () (_ BitVec 256))
+(declare-fun x47 () (_ BitVec 256))
+(declare-fun x1 () (_ BitVec 256))
+(declare-fun x33 () (_ BitVec 256))
+(declare-fun x23 () (_ BitVec 256))
+(declare-fun x57 () (_ BitVec 256))
+(declare-fun x17 () (_ BitVec 256))
+(declare-fun x14 () Bool)
+(declare-fun x40 () (_ BitVec 256))
+(declare-fun x72 () (_ BitVec 256))
+(declare-fun x24 () (_ BitVec 256))
+(declare-fun x26 () (_ BitVec 256))
+(declare-fun x59 () (_ BitVec 256))
+(declare-fun x83 () (_ BitVec 256))
+(declare-fun x49 () (_ BitVec 256))
+(declare-fun x12 () (_ BitVec 256))
+(declare-fun x34 () (_ BitVec 256))
+(declare-fun x13 ((_ BitVec 256) (_ BitVec 256) (_ BitVec 256)) (_ BitVec 256))
+(declare-fun x79 () (_ BitVec 256))
+(declare-fun x67 () (_ BitVec 256))
+(declare-fun x69 () (_ BitVec 256))
+(declare-fun x51 () (_ BitVec 256))
+(declare-fun x44 () (_ BitVec 256))
+(declare-fun x53 () Bool)
+(declare-fun x18 ((_ BitVec 256)) (_ BitVec 256))
+(declare-fun x30 () (_ BitVec 256))
+(declare-fun x8 () (_ BitVec 256))
+(declare-fun x50 () Bool)
+(declare-fun x81 () (_ BitVec 256))
+(declare-fun x28 () (_ BitVec 256))
+(declare-fun x43 () (_ BitVec 256))
+(declare-fun x46 () (_ BitVec 256))
+(declare-fun x80 () (_ BitVec 256))
+(declare-fun x37 () (_ BitVec 256))
+(declare-fun x36 () (_ BitVec 256))
+(declare-fun x20 () (_ BitVec 256))
+(declare-fun x19 () (_ BitVec 256))
+(declare-fun x32 () Bool)
+(declare-fun x31 () (_ BitVec 256))
+(declare-fun x82 () (_ BitVec 256))
+(declare-fun x29 () (_ BitVec 256))
+(declare-fun x52 ((_ BitVec 256)) (_ BitVec 256))
+(declare-fun x76 () (_ BitVec 256))
+(define-fun x78 ((x39 (_ BitVec 256)) (x6 (_ BitVec 256))) Bool (= x39 (bvudiv (bvmul x6 x39) x6)))
+(define-fun x38 ((x39 (_ BitVec 256)) (x6 (_ BitVec 256))) Bool (= x39 (bvsdiv (bvmul x39 x6) x6)))
+(define-fun x16 ((x39 (_ BitVec 256)) (x6 (_ BitVec 256))) Bool (= x39 (bvsdiv (bvmul x6 x39) x6)))
+(define-fun x60 ((x55 (_ BitVec 256))) (_ BitVec 256) (ite (= x55 x46) x71 (x77 x55)))
+(assert (=> (bvule x46 (_ bv10000 256)) (= (x18 x46) (_ bv0 256))))
+(assert (= (_ bv64 256) (x21 (x13 (_ bv64 256) x31 (_ bv2 256)))))
+(assert (not (x45 (x13 (_ bv64 256) x19 (_ bv2 256)))))
+(assert (x45 (_ bv4294967295 256)))
+(assert (x45 (_ bv115792089237316195423570985008687907853269984665640564039457 256)))
+(assert (=> (bvuge (_ bv10000 256) x23) (= (_ bv0 256) (x18 x23))))
+(assert (bvugt (x13 (_ bv64 256) x31 (_ bv2 256)) (_ bv10000 256)))
+(assert (= (_ bv0 256) (x18 (_ bv57896044618658097711785492504343953926634992332820282019728792003956564819967 256))))
+(assert (= (x18 (_ bv404098525 256)) (_ bv0 256)))
+(assert (= (_ bv0 256) (x18 (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256))))
+(assert (= (_ bv0 256) (x18 (_ bv1889567281 256))))
+(assert (= x31 (x75 (x13 (_ bv64 256) x31 (_ bv2 256)))))
+(assert (= (_ bv0 256) (x18 (_ bv115792089237316195423570985008687907853269984665640564039457 256))))
+(assert (=> (bvuge (_ bv10000 256) x19) (= (_ bv0 256) (x18 x19))))
+(assert (= (x13 (_ bv64 256) x31 (_ bv2 256)) (x18 (x13 (_ bv64 256) x31 (_ bv2 256)))))
+(assert (= (x75 (x13 (_ bv64 256) x19 (_ bv2 256))) x19))
+(assert (= (x18 (x13 (_ bv64 256) x19 (_ bv2 256))) (x13 (_ bv64 256) x19 (_ bv2 256))))
+(assert (= (x18 (_ bv1289409798 256)) (_ bv0 256)))
+(assert (x45 (_ bv649617121 256)))
+(assert (= (x48 (x13 (_ bv64 256) x19 (_ bv2 256))) (_ bv2 256)))
+(assert (=> (bvule x31 (_ bv10000 256)) (= (_ bv0 256) (x18 x31))))
+(assert (= (x18 (_ bv105312291668557186697918027683670432318895095400549111254310977535 256)) (_ bv0 256)))
+(assert (not (x45 (x13 (_ bv64 256) x31 (_ bv2 256)))))
+(assert (x45 (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256)))
+(assert (x45 (_ bv1289409798 256)))
+(assert (= (_ bv64 256) (x21 (x13 (_ bv64 256) x19 (_ bv2 256)))))
+(assert (= (_ bv0 256) (x18 (_ bv1461501637330902918203684832716283019655932542975 256))))
+(assert (not x5))
+(assert (= (x18 (_ bv649617121 256)) (_ bv0 256)))
+(assert (= (x18 (_ bv1000000000000000000 256)) (_ bv0 256)))
+(assert (x45 (_ bv1889567281 256)))
+(assert (x45 (_ bv105312291668557186697918027683670432318895095400549111254310977535 256)))
+(assert (x45 (_ bv1461501637330902918203684832716283019655932542975 256)))
+(assert (x45 (_ bv1000000000000000000 256)))
+(assert (= (x18 (_ bv4294967295 256)) (_ bv0 256)))
+(assert (=> (bvuge (_ bv10000 256) x47) (= (_ bv0 256) (x18 x47))))
+(assert (= true x32))
+(assert (bvult (_ bv10000 256) (x13 (_ bv64 256) x19 (_ bv2 256))))
+(assert (x45 (_ bv404098525 256)))
+(assert (= (_ bv2 256) (x48 (x13 (_ bv64 256) x31 (_ bv2 256)))))
+(assert (=> (bvuge (_ bv10000 256) x20) (= (x18 x20) (_ bv0 256))))
+(assert (x45 (_ bv57896044618658097711785492504343953926634992332820282019728792003956564819967 256)))
+(assert (= x5 (=> (and (and (bvuge (_ bv1461501637330902918203684832716283019655932542975 256) x47) (bvule (_ bv0 256) x25) (= x33 (_ bv0 256)) (bvuge x9 (_ bv0 256)) (bvule x20 (_ bv1461501637330902918203684832716283019655932542975 256)) (= x50 (bvugt (x61 x23) (_ bv0 256))) (bvule x11 (_ bv57896044618658097711785492504343953926634992332820282019728792003956564819967 256)) (bvuge x47 (_ bv1 256)) (bvuge (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256) x59) (= (bvugt (x61 x20) (_ bv0 256)) x53) (bvuge (_ bv4294967295 256) x73) (not (= x23 x20)) (bvule (_ bv0 256) x70) (= x27 (_ bv4 256)) x4 (not (= x20 x47)) (bvuge x59 (_ bv0 256)) (= x34 (_ bv404098525 256)) (bvule x70 (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256)) (bvule x23 (_ bv1461501637330902918203684832716283019655932542975 256)) (bvuge x23 (_ bv1 256)) (bvule (_ bv4 256) x11) (bvule (_ bv0 256) x8) (= x30 (x61 x20)) (= (bvult (_ bv0 256) (x61 x47)) x4) (bvuge x7 (_ bv0 256)) (bvule x7 (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256)) (bvule (_ bv1 256) x20) (bvule (_ bv0 256) x73) (bvuge (_ bv1461501637330902918203684832716283019655932542975 256) x67) (= (_ bv36 256) x1) (bvule (_ bv0 256) x12) (bvuge x30 (_ bv1 256)) (bvule x57 (_ bv115792089237316195423570985008687907853269984665640564039457 256)) (bvule (_ bv0 256) x67) x50 (not (= x23 x47)) (bvule x62 (_ bv1461501637330902918203684832716283019655932542975 256)) (bvuge (_ bv1461501637330902918203684832716283019655932542975 256) x9) (bvuge (_ bv1461501637330902918203684832716283019655932542975 256) x65) (bvule x25 (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256)) x53 (bvule (_ bv0 256) x65) (bvuge (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256) x8) (bvule (_ bv0 256) x62) (bvule x12 (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256))) (and (and (= (_ bv36 256) x80) (= x57 x69) (= x29 (bvudiv x17 (_ bv1000000000000000000 256))) (bvule (_ bv1 256) x15) (= x17 (bvmul x69 (_ bv1000000000000000000 256))) (= (bvudiv x17 x74) x82) (= x69 x29) (= x10 (_ bv1289409798 256)) (= x69 x2) (bvule (_ bv1 256) x74) (bvule x74 (_ bv105312291668557186697918027683670432318895095400549111254310977535 256)) (= x15 (x61 x20))) (and (and (= x28 (x61 x23)) x35 (= x49 (x13 (_ bv64 256) x31 (_ bv2 256))) (= (bvule x82 x58) x35) (= x31 x84) (= (_ bv1889567281 256) x63) (= x20 x31) (bvule (_ bv1 256) x28) (= (x52 x49) x58)) (and (and (= (x61 x20) x66) (= (_ bv404098525 256) x56) (bvuge x66 (_ bv1 256)) (= (x60 x23) x83) (= x68 (_ bv4 256)) (= x24 (_ bv649617121 256)) (= x81 (_ bv36 256)) (= x71 x79) (= x71 (x77 x46)) (= x37 x83) (= (x61 x23) x40) (bvuge x40 (_ bv1 256)) (= x46 x9)) (and (and (= x64 x36) (= x72 (bvudiv x76 x74)) (bvule (_ bv1 256) x54) (= x42 (_ bv36 256)) (= (bvmul (_ bv1000000000000000000 256) x64) x76) (= x64 x26) (= (x61 x20) x54) (= x57 x64) (= x36 (bvudiv x76 (_ bv1000000000000000000 256))) (= x22 (_ bv1289409798 256))) (and (bvuge x44 (_ bv1 256)) (= x19 x43) (= x20 x19) (= x3 (x52 x41)) (= (x61 x23) x44) (= (x13 (_ bv64 256) x19 (_ bv2 256)) x41) (= x14 (bvuge x3 x72)) (= x51 (_ bv1889567281 256)))))))) x14)))
+(check-sat)
+(exit)