This site provides our paper Scaling Up DPLL(T) String Solvers using Context-Dependent Simplification and related material at CAV 2017.
To enable individual configurations of CVC4:
Our evaluation used the StarExec cluster for evaluation. We provide a spreadsheet results-cav17.xlsx containing detailed results of the experiments. The columns of this spreadsheet show all benchmark/solver pairs, as well as various additional tests to verify the correctness of models produced by z3 and cvc4, on benchmarks where solvers gave different answers, including timeouts. For instance the column “z3 : +cvc4-m” indicates the result of z3 on the original benchmark plus constraints corresponding to cvc4’s model. The scripts used to test the consistency of models can be found here.