Skip to content
A simple scrambler for SMT-LIB 2.6 scripts.
C++ SMT Shell Makefile
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
test
.clang-format
.travis.yml
COPYING
Makefile
README.md
lexer.l
parser.y
process.incremental-track
process.model-val-track
process.single-query-challenge-track
process.unsat-core-track
scrambler.cpp
scrambler.h

README.md

License: MIT Build Status

SMT-COMP Benchmark Scrambler

This is the official SMT-COMP benchmark scrambler, used as a pre-processor for all tracks of SMT-COMP.

Known limitations

Benchmarks that contain deeply nested terms require a large stack to be scrambled. (This is caused by the recursive implementation of benchmark printing, which recurses over each term's parse tree.) The default stack size of 8192 KB on Linux systems is sufficient for terms with a depth of about 80,000. Some benchmarks in SMT-LIB do contain more deeply nested terms. To process such benchmarks, the stack limit needs to be increased (using, e.g., `ulimit -s 131072) before the scrambler is invoked. Otherwise, the scrambler may cause a segmentation fault.

Usage

Single-Query Track and Industry Challenge Track

See process.single-query-challenge-track.

ulimit -s 131072
./scrambler -seed <seed> < <benchmark>

Incremental Track

See process.incremental-track.

# extract the expected results of check-sat commands and prepend them
# to the scrambled benchmark (in their original order) -- this format
# is expected by the trace executor
grep 'set-info :status' "$1"|sed 's/(set-info :status \(.*\))/\1/'
echo "--- BENCHMARK BEGINS HERE ---"
ulimit -s 131072
./scrambler -seed <seed> < <benchmark>

Model-Validation Track

See process.model-val-track.

ulimit -s 131072
./scrambler -seed <seed> -gen-model-val true < <benchmark>

Unsat-Core Track

See process.unsat-core-track.

ulimit -s 131072
./scrambler -seed <seed> -gen-unsat-core true < <benchmark>
You can’t perform that action at this time.