Code

Fix rosetta binary search#1481

Code

Merged

vakaras merged 7 commits intomasterviperproject/prusti-dev:masterfrom fix-rosetta-binary-searchviperproject/prusti-dev:fix-rosetta-binary-searchCopy head branch name to clipboardDec 8, 2023

+801

Commits

Commits on Dec 8, 2023

• Add original Binary Search Rosetta examples from the artefact.

  vakaras

  committed
  140aa99

  Copy full SHA for 140aa99

• Update the original Binary Search Rosetta examples to use new syntax.

  vakaras

  committed
  fe74872

  Copy full SHA for fe74872

• Add Binary Search Rosetta examples with fixed termination bugs.

  vakaras

  committed
  ac7d11a

  Copy full SHA for ac7d11a

• Move Binary Search examples to the right folder.

  vakaras

  committed
  b0d7817

  Copy full SHA for b0d7817

• Verify Binary Search Rosetta Generic that the found element is correct.

  vakaras

  committed
  3e15558

  Copy full SHA for 3e15558

• Verify Binary Search Rosetta Generic that if no element found, it does not exist.

  vakaras

  committed
  9567ddd

  Copy full SHA for 9567ddd

• Disable more complete exhale.

  vakaras

  committed
  fdf4811

  Copy full SHA for fdf4811