goto-cc Homepage Compiling GOTO-Programs
About -- Download -- Examples -- Documentation

Instructions to compile freecell-solver to a GOTO-object

Latest version of example sources known to work: 2.8.12
Latest version of goto-cc known to work on this example: 2.5
  1. Download the freecell-solver sources and unpack the files.

    tar xfz freecell-solver-2.8.12.tar.gz

  2. Switch to the freecell-solver-2.8.12 directory

    cd freecell-solver-2.8.12

    and configure the build like this:

    ./configure CC="goto-cc --i386-linux" --host=none-none-none

  3. Make it!

    make

    The result will be a file called fc-solve (the main freecell solver) and another example binary called freecell-solver-range-parallel-solve

  4. Try to verify the program by using the final object file in CBMC or SATABS:

    cbmc --binary fc-solve

    Of course you will need different options if you want to check the program for a special claim or if you're using a different tool.