Wiki¶

Folders in the Benchmark Set¶

The folders are divided into 3 categories.

• /main-bench: where are all the working or suppose to work benchmarks. Please add here any new benchmark that you have and works (instead of sending it via email).
• /challenge-bench: where are all the benchmarks with no encoding to SMT support exists. If you add a new functionality please do check if there are some benchmarks here that can be in main-bench.
• /raw-code-examples: if you have a new set of benchmarks that we shall start work on and check, please add it here.

Folders in the Main Benchmark Set¶

Before start testing, please first check HiFrog is running at all: ./hifrog --help

Later you may use these tests to check basic and advanced functionality of HiFrog:

• To test that basic things are working in HiFrog, use these sets: /main-bench/arithmetic, /main-bench/branching, /main-bench/convertions, /main-bench/counter_example, and /main-bench/inject_summaries.
• Regression tests: /main-bench/funfrog_regression and /main-bench/sv-comp16.
• More complicated test: /main-bench/sv-comp16 and /main-bench/milano-bicocca-bench.