A docker image is provided to run the instrumented solver and the checker, you can download it using the following link: Download
Docker Image Guidelines:
Load the image from the downloaded tar archive using the command:
docker image load -i tswc-dac21.tar.gz
You can simply run an interactive shell container using that image and explore image content using the command:
docker run -it tswc-dac21 bash
To execute the instrumented solver: use "opensmt file", with "file" being the path to the smt2 instance. All certificates will be generated in the ./proof folder, located in the folder from which the call is made.
../tswc.sh ./proof ../modules QF_LRA
terminates with the message "verified - all certificates are valid" and all certificates being stored in the "example/proof" folder.
and copy [smt2-instance] to the [instance-folder] using
docker cp [smt2-instance] [container-id]:/home/[instance-folder]/[smt2-instance]
and finally use "cd [instance-folder]; opensmt [smt2-instance]; ../tswc.sh ./proof ../modules [Theory]" to generate your certificates.