Files

.githooks
.github
cmake
doc
integration
jbmc
regression
- acceleration
- ansi-c
- array-refinement-with-incr
- book-examples
- catch-framework
- cbmc-concurrency
- cbmc-cover
- cbmc-cpp
- cbmc-incr-oneloop
- cbmc-incr-smt2
- cbmc-incr
- cbmc-library
- cbmc-output-file
- cbmc-primitives
- cbmc-sequentialization
- cbmc-shadow-memory
- cbmc-with-incr
- cbmc
- contracts-dfcc
- contracts
- cpp-linter
- cpp
- cprover
  - arrays
  - aws-c-common
  - basic
  - branching
  - contracts
  - cstrings
  - float
  - function_calls
  - function_pointers
  - large_step
    - arrays
      - array1.c
      - array1.desc
      - array2.c
      - array2.desc
      - array4.c
      - array4.desc
      - array_literal1.c
      - array_literal1.desc
      - array_literal2.c
      - array_r_ok1.c
      - array_r_ok1.desc
      - array_set1.c
      - array_set1.desc
      - iterate_over_array1.c
      - iterate_over_array1.desc
      - iterate_over_array2.c
      - iterate_over_array2.desc
    - aws-c-common
    - basic
    - branching
    - contracts
    - cstrings
    - float
    - function_calls
    - function_pointers
    - lists
    - loops
    - pointers
    - quantifiers
    - safety
    - structs
    - trace
    - unions
    - CMakeLists.txt
    - Makefile
  - lists
  - loops
  - pointers
  - quantifiers
  - safety
  - structs
  - trace
  - unions
  - CMakeLists.txt
  - Makefile
- crangler
- extract_type_header
- goto-analyzer-simplify
- goto-analyzer-taint
- goto-analyzer
- goto-bmc
- goto-cc-cbmc
- goto-cc-file-local
- goto-cc-goto-analyzer
- goto-cc-multi-file
- goto-cc-regression-gh-issue-5380
- goto-cl
- goto-diff
- goto-gcc
- goto-harness-multi-file-project
- goto-harness
- goto-inspect
- goto-instrument-chc
- goto-instrument-json
- goto-instrument-typedef
- goto-instrument-wmm-core
- goto-instrument
- goto-interpreter
- goto-ld
- goto-synthesizer
- invariants
- k-induction
- libcprover-cpp
- linking-goto-binaries
- memory-analyzer
- smt2_solver
- smt2_strings
- snapshot-harness
- solver-hardness
- statement-list
- strings
- symtab2gb-cbmc
- symtab2gb
- systemc
- test-script
- validate-trace-xml-schema
- .gitignore
- CMakeLists.txt
- Makefile
- README.md
- test.pl
scripts
src
unit
.clang-format
.clang-format-ignore
.dir-locals.el
.editorconfig
.gitattributes
.gitignore
.gitmodules
CHANGELOG
CMakeLists.txt
CODEOWNERS
CODING_STANDARD.md
COMPILING.md
Dockerfile
FEATURE_IDEAS.md
LICENSE
README.md
RELEASE_PROCESS.md
TOOLS_OVERVIEW.md

iterate_over_array2.desc

This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Yakir Vizel

and

Adding regression tests for large step encoding of CHCs

Feb 24, 2025

7638533 · Feb 24, 2025