File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 11.PHONY : clean all test
22
3+ YEAR =2022
34CFLAGS =-g -O3
45LDFLAGS =
5- DISTFILES =SMT-COMP-2021 -trace-executor.tar.gz
6+ DISTFILES =SMT-COMP-$( YEAR ) -trace-executor.tar.gz
67
78all : $(DISTFILES )
89
@@ -12,7 +13,7 @@ smtlib2_trace_executor: smtlib2_trace_executor.o
1213clean :
1314 rm -f smtlib2_trace_executor.o smtlib2_trace_executor $(DISTFILES ) test_solver_log.txt
1415
15- SMT-COMP-2021 -trace-executor.tar.gz : starexec_run_default smtlib2_trace_executor
16+ SMT-COMP-$( YEAR ) -trace-executor.tar.gz : starexec_run_incremental smtlib2_trace_executor
1617 tar -czf $@ $^
1718
1819test : smtlib2_trace_executor
Original file line number Diff line number Diff line change @@ -58,19 +58,20 @@ incremental track where the trace-executor needs to interact with your
5858solver. Instead the solution for SMT-COMP is to add the
5959trace executor to the solver binaries and upload a wrapped solver.
6060Note that in the competition the SMT-COMP organizers will wrap your
61- solver. These instructions are meant to help solver authors to test
62- their solvers on starexec before the competition.
61+ solver if you do not wrap it yourself. These instructions are meant
62+ to help solver authors to test their solvers on starexec before the
63+ competition.
6364
6465To wrap your solver, first follow the above instructions for the
6566Docker build or download the released tar archive. Then rename your
6667solver's start script and extract the tar archive.
6768
6869``` sh
6970cd mysolver/bin
70- mv starexec_run_* original_starexec_run_default
71+ test -e smtcomp_run_incremental || mv starexec_run_* smtcomp_run_incremental
7172tar -xzf .../SMT-COMP-20* -trace-executor.tar.gz
7273```
7374
74- Upload the wrapped solver to starexec. Note that the wrapped solver
75- can only be used in the incremental track with the incremental
76- scrambler and post-processor.
75+ Upload the wrapped solver to starexec. Note that this creates a
76+ new configuration that must be used with the incremental scrambler
77+ and post-processor.
Load Diff This file was deleted.
Original file line number Diff line number Diff line change 1+ #! /bin/sh
2+
3+ ./smtlib2_trace_executor --continue-after-unknown ./smtcomp_run_incremental " $1 "
You can’t perform that action at this time.
0 commit comments