README ============================================================================== Counterexample-Guided Model Synthesis (TACAS 2017) Mathias Preiner, Aina Niemetz, Armin Biere ============================================================================== ------------------------------------------------------------------------------ 1 - Materials provided ------------------------------------------------------------------------------ + boolector ------------------------ the solver binary used in the evaluation + configuration Btor: ------------------- CEGMS without model synthesis enabled + configuration Btor+s: --------------------- CEGMS with model synthesis enabled + configuration Btor+d: --------------------- dual CEGMS without model synthesis enabled + configuration Btor+ds: ---------------------- dual CEGMS with model synthesis enabled + tacas17-BV_LNIRA.7z ------------------------ Contains all 4838 LIA, LRA, NIA, NRA benchmarks from SMT-LIB translated into BV. + runs ------------------------ Contains all log files of our experimental evaluation used for this paper. Each directory representing a run contains an 'options' file, listing all the options passed to the solver binary used in this run. ------------------------------------------------------------------------------ 2 - Experimental Setup ------------------------------------------------------------------------------ All our experiments were conducted on a cluster of 30 nodes of 2.83GHz Intel Core 2 Quad machines with 8GB of memory using Ubuntu 14.04.5 LTS. As a memory limit, we used 7GB. As a CPU time limit, we used 1200 seconds. Note that the provided log files of the runs of Btor+d, Btor+ds, and Q3B were produced using a CPU time limit of 2400 seconds (1200 seconds per thread/process). The results in the paper were compiled based on a CPU time limit of 1200s.