On Simplification of Formulas with Unconstrained Variables and Quantifiers

1. Z3
- 1.1. SMT-LIB
- 1.2. SymDIVINE
2. Q3B
- 2.1. SMT-LIB
- 2.2. SymDIVINE
3. Boolector
- 3.1. SMT-LIB
- 3.2. SymDIVINE
4. Simplification times
5. Data files

This document summarizes experimental evaluation of ellimination of unconstrained variables from quantified bit-vector formulas. This is the additional material to the paper On Simplification of Formulas with Unconstrained Variables and Quantifiers, which was submitted to the conference SAT 2017.

The evaluation is performed on three data sets:

SMT-LIB is a set of benchmarks by Christoph M. Wintersteiger obtained from hardware verification problems,
SymDIVINE is a set of benchmarks obtained by evaluating the model checker SymDIVINE on benchmarks from SV-COMP.

Two configurations are tested:

running the solver on the original benchmark after cheap Z3 simplifications,
simplifying the benchmark by removing unconstrained variables and simple Z3 simplifications up to the fixed point and running the solver.

Evaluation of experiments is done in R. All scripts used are contained in this document. Links to data files in the CSV format are available in the respective section.

We need to load several R packages:

library(plyr)
library(ggplot2)
library(scales)
library(colorspace)
library(RColorBrewer)

1 Z3

1.1 SMT-LIB

1.1.1 Load the results

First, lets get the data and merge them.

simplTimes <- read.csv("simpltimes_smtlib.csv", header=TRUE, stringsAsFactors=FALSE)
smtlib.z3 <- read.csv("z3_smtlib.csv", header=TRUE, stringsAsFactors=FALSE)
smtlib.z3_u <- read.csv("z3_smtlib_unconstrained.csv", header=TRUE, stringsAsFactors=FALSE)

smtlib <- Reduce(function(x, y) merge(x, y, all=TRUE, by="filename"), list(smtlib.z3, smtlib.z3_u, simplTimes))
colnames(smtlib) = c('filename', 'result', 'cputime', 'walltime', 'memusage', 'result.u', 'cputime.u', 'walltime.u', 'memusage.u', 'simpltime')

smtlib$cputime[smtlib$result != "sat" & smtlib$result != "unsat"] <- 900
smtlib$walltime[smtlib$result != "sat" & smtlib$result != "unsat"] <- 900
smtlib$cputime.u[smtlib$result.u != "sat" & smtlib$result.u != "unsat"] <- 900
smtlib$walltime.u[smtlib$result.u != "sat" & smtlib$result.u != "unsat"] <- 900

Now, compare number of results of each type for each configuration.

smtlib_standard <- count(smtlib.z3, "result")
colnames(smtlib_standard) <- c('result', 'standard')

smtlib_unconstrained <- count(smtlib.z3_u, "result")
colnames(smtlib_unconstrained) <- c('result', 'unconstrained')

Reduce(function(...) merge(..., all=TRUE),
         list(smtlib_standard, smtlib_unconstrained))

result	standard	unconstrained
out of memory	7	nil
sat	70	72
timeout	22	27
unsat	92	92

1.1.2 Result counts

This table shows numbers of benchmarks grouped by the result in both of the configurations.

count(smtlib, c('result', 'result.u'))

result	result.u	freq
out of memory	timeout	7
sat	sat	70
timeout	sat	2
timeout	timeout	20
unsat	unsat	92

1.1.3 Total time/memory

Now, lets see the total CPU time, wall time, memory used and simplification times for both of the configurations.

numcolwise(sum)(smtlib[which((smtlib$result == "sat" & smtlib$result.u == "sat") | (smtlib$result == "unsat" & smtlib$result.u == "unsat")),])

cputime	walltime	memusage	cputime.u	walltime.u	memusage.u	simpltime
425.902616885	429.77246453613	1289932800	430.445301965	439.247484471649	1219837952	13.2316562775522

1.1.4 Scatter plots

Linear scale

ggplot(smtlib, aes(cputime, cputime.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained", xlim=c(0.001,900), ylim=c(0.001,900)) +
  geom_point() +
  geom_abline(intercept=0) +
  theme(legend.title=element_blank())

Log scale

ggplot(smtlib, aes(cputime, cputime.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained", xlim=c(0.001,900), ylim=c(0.001,900)) +
  geom_point() +
  geom_abline(intercept=0) +
  scale_x_log10(limits = c(0.001, 900), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(limits = c(0.001, 900), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  theme(legend.title=element_blank())

Log scale + simplification time

ggplot(smtlib, aes(cputime, cputime.u + simpltime, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained", xlim=c(0.001,900), ylim=c(0.001,900)) +
  geom_point() +
  geom_abline(intercept=0) +
  scale_x_log10(limits = c(0.001, 900), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(limits = c(0.001, 900), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  theme(legend.title=element_blank())

Memory

ggplot(smtlib, aes(memusage, memusage.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained") +
  geom_point() +
  geom_abline(intercept=0) +
  scale_x_log10(limits = c(1000000,8000000000), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(limits = c(1000000,8000000000), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  theme(legend.title=element_blank())

1.1.5 Quantile plot

smtlib.ordered = sort(smtlib$cputime[smtlib$result == "sat" | smtlib$result == "unsat"]);
smtlib.ordered.u = sort(smtlib$cputime.u[smtlib$result.u == "sat" | smtlib$result.u == "unsat"]);
smtlib.ordered.us = sort((smtlib$cputime.u + smtlib$simpltime)[smtlib$result.u == "sat" | smtlib$result.u == "unsat"]);

plot(c(0, 160), c(0.001, 900), log='y', xlab=NA, ylab=NA, axes=FALSE, frame.plot=TRUE, type='n')

axis(1, at=seq(0,200,50), tck = -.01, label=NA)
axis(2, at=c(0.001,0.1,1,10,100), tck = -.01, label=NA)
axis(1, at=seq(0,200,50), lwd = 0, line = -.8)
axis(2, at=c(0.001,0.01,0.1,1,10,100), labels=c(0.001,0.01,0.1,1,10,100), lwd = 0, line = -.4, las = 1)

lines(1:length(smtlib.ordered), smtlib.ordered, type='s', col='blue')
lines(1:length(smtlib.ordered.u), smtlib.ordered.u, type='s', col='darkgreen')
lines(1:length(smtlib.ordered.us), smtlib.ordered.us, type='s', col='red')

mtext(side = 1, "Formulas from SMT-LIB solved by Z3", line = 1.2)
mtext(side = 2, "CPU time (s)", line = 2)

legend("topleft",
  lty=c(1,1,1),
  lwd=c(2.5,2.5,2.5),
  col=c("blue", "darkgreen", "red"),
  legend=c("standard", "unconstrained", "unconstrained+simplification time"))

1.1.6 Degraded performance

These are the results where the simplifications increase the solving time by more than 0.5 s.

smtlib[smtlib$cputime + 0.5 < smtlib$cputime.u, c('filename', 'cputime', 'cputime.u')]

filename	cputime	cputime.u
ranking/893016/audio_ac97_wavepcistream.cpp.smt2	356.622124514	381.158789738
ranking/893063/general_pcidrv_sys_hw_eeprom.c.smt2	0.407706638	1.144467538

1.1.7 Improved performance

These are the results where the simplifications decrease the solving time by more than 0.5 s.

smtlib[smtlib$cputime.u + 0.5 < smtlib$cputime, c('filename', 'cputime', 'cputime.u')]

filename	cputime	cputime.u
fixpoint/893182/sdlx-fixpoint-5.smt2	4.466734446	1.647817043
ranking/893022/filesys_cdfs_namesup_noarray.c.smt2	5.668319623	3.74251238
ranking/893037/kmdf_usbsamp_sys_queue.c.smt2	900	0.038231728
ranking/893052/network_irda_miniport_nscirda_settings.c.smt2	13.982148116	0.223287671
ranking/893053/1394diag_ioctl.c.smt2	900	33.001279091
ranking/893066/network_irda_miniport_nscirda_comm.c.smt2	3.545393268	1.748568861

1.2 SymDIVINE

1.2.1 Load the results

First, lets get the data and merge them.

simplTimes <- read.csv("simpltimes_symdivine.csv", header=TRUE, stringsAsFactors=FALSE)
symdivine.z3 <- read.csv("z3_symdivine.csv", header=TRUE, stringsAsFactors=FALSE)
symdivine.z3_u <- read.csv("z3_symdivine_unconstrained.csv", header=TRUE, stringsAsFactors=FALSE)

symdivine <- Reduce(function(x, y) merge(x, y, all=TRUE, by="filename"), list(symdivine.z3, symdivine.z3_u, simplTimes))
colnames(symdivine) = c('filename', 'result', 'cputime', 'walltime', 'memusage', 'result.u', 'cputime.u', 'walltime.u', 'memusage.u', 'simpltime')

symdivine$cputime[symdivine$result != "sat" & symdivine$result != "unsat"] <- 900
symdivine$walltime[symdivine$result != "sat" & symdivine$result != "unsat"] <- 900
symdivine$cputime.u[symdivine$result.u != "sat" & symdivine$result.u != "unsat"] <- 900
symdivine$walltime.u[symdivine$result.u != "sat" & symdivine$result.u != "unsat"] <- 900

Now, compare number of results of each type for each configuration.

symdivine_standard <- count(symdivine.z3, "result")
colnames(symdivine_standard) <- c('result', 'standard')

symdivine_unconstrained <- count(symdivine.z3_u, "result")
colnames(symdivine_unconstrained) <- c('result', 'unconstrained')

Reduce(function(...) merge(..., all=TRUE),
         list(symdivine_standard, symdivine_unconstrained)) #, symdivine_localunconstrained))

result	standard	unconstrained
out of memory	203	5
sat	1137	1137
timeout	125	125
unsat	3996	4194

1.2.2 Result counts

This table shows numbers of benchmarks grouped by the result in both of the configurations.

count(symdivine, c('result', 'result.u'))

result	result.u	freq
out of memory	out of memory	5
out of memory	unsat	198
sat	sat	1137
timeout	timeout	125
unsat	unsat	3996

1.2.3 Total time/memory

Now, lets see the total CPU time, wall time, memory used and simplification times for both of the configurations.

numcolwise(sum)(symdivine[which((symdivine$result == "sat" & symdivine$result.u == "sat") | (symdivine$result == "unsat" & symdivine$result.u == "unsat")),])

cputime	walltime	memusage	cputime.u	walltime.u	memusage.u	simpltime
3006.450193861	3347.73343639821	137585696768	380.924227113	788.743877772242	9889116160	130.815435322002

1.2.4 Scatter plots

Linear scale

ggplot(symdivine, aes(cputime, cputime.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained", xlim=c(0,900), ylim=c(0,900)) +
  geom_point() +
  geom_abline(intercept=0) +
  theme(legend.title=element_blank())

Log scale

ggplot(symdivine, aes(cputime, cputime.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained") +
  geom_point() +
  geom_abline(intercept=0) +
  scale_x_log10(limits = c(0.001, 900), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(limits = c(0.001, 900), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  theme(legend.title=element_blank())

Log scale + simplification time

ggplot(symdivine, aes(cputime, cputime.u+simpltime, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained") +
  geom_point() +
  geom_abline(intercept=0) +
  scale_x_log10(name="Z3", limits = c(0.001, 901), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(name="Z3 + simplifications", limits = c(0.001, 901), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  theme(legend.title=element_blank()) +
  scale_colour_brewer(palette = "Set1") +
  theme(legend.position="none")

1.2.5 Memory

ggplot(symdivine, aes(memusage, memusage.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained", log="xy", xlim=c(1000000,8000000000), ylim=c(1000000,8000000000)) +
  geom_point() +
  geom_abline(intercept=0) +
  scale_x_log10(breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  theme(legend.title=element_blank())

1.2.6 Quantile plot

symdivine.ordered = sort(symdivine$cputime[symdivine$result == "sat" | symdivine$result == "unsat"]);
symdivine.ordered.u = sort(symdivine$cputime.u[symdivine$result.u == "sat" | symdivine$result.u == "unsat"]);
symdivine.ordered.us = sort((symdivine$cputime.u + symdivine$simpltime)[symdivine$result.u == "sat" | symdivine$result.u == "unsat"]);

plot(c(0, 5500), c(0.001, 900), log='y', xlab=NA, ylab=NA, axes=FALSE, frame.plot=TRUE, type='n')

axis(1, at=seq(0,5500,500), tck = -.01, label=NA)
axis(2, at=c(0.001,0.1,1,10,100), tck = -.01, label=NA)
axis(1, at=seq(0,5500,500), lwd = 0, line = -.8)
axis(2, at=c(0.001,0.01,0.1,1,10,100), labels=c(0.001,0.01,0.1,1,10,100), lwd = 0, line = -.4, las = 1)

lines(1:length(symdivine.ordered), symdivine.ordered, type='s', col='blue')
lines(1:length(symdivine.ordered.u), symdivine.ordered.u, type='s', col='darkgreen')
lines(1:length(symdivine.ordered.us), symdivine.ordered.us, type='s', col='red')

mtext(side = 1, "Formulas from SymDIVINE solved by Z3", line = 1.2)
mtext(side = 2, "CPU time (s)", line = 2)

legend("topleft",
  lty=c(1,1,1),
  lwd=c(2.5,2.5,2.5),
  col=c("blue", "darkgreen", "red"),
  legend=c("standard", "unconstrained", "unconstrained+simplification time"))

1.2.7 Degraded performance

These are the results where the simplifications increase the solving time by more than 0.5 s.

symdivine[symdivine$cputime + 0.5 < symdivine$cputime.u, c('filename', 'cputime', 'cputime.u')]

filename

cputime

cputime.u

1.2.8 Improved performance

These are the results where the simplifications decrease the solving time by more than 0.5 s.

symdivine[symdivine$cputime.u + 0.5 < symdivine$cputime, c('filename', 'cputime', 'cputime.u')]

filename	cputime	cputime.u
bitvector/gcd_3_true.ll/54.smt2	12.98061248	12.315526886
bitvector/gcd_3_true.ll/72.smt2	10.946924788	10.443508681
eca/Problem01_00_true.ll/2825.smt2	2.848532975	0.011955775
eca/Problem01_00_true.ll/4074.smt2	2.861864428	0.011991767
eca/Problem01_00_true.ll/5092.smt2	10.551358451	0.01306112
eca/Problem01_00_true.ll/5300.smt2	10.524900394	0.013130108
eca/Problem01_00_true.ll/6239.smt2	10.47834444	0.013828855
eca/Problem01_10_true.ll/4273.smt2	1.294254087	0.010639634
eca/Problem01_10_true.ll/4515.smt2	10.544314342	0.0120098
eca/Problem01_10_true.ll/5464.smt2	10.471055421	0.010030681
eca/Problem01_10_true.ll/5489.smt2	10.576945116	0.011367564
eca/Problem01_10_true.ll/5642.smt2	1.28490532	0.011352392
eca/Problem01_20_false.ll/2267.smt2	1.270555521	0.009226606
eca/Problem01_20_false.ll/3946.smt2	10.480970188	0.011168633
eca/Problem01_20_false.ll/5888.smt2	10.589594764	0.012016012
eca/Problem01_20_false.ll/6033.smt2	10.571111364	0.011956579
eca/Problem01_20_false.ll/6092.smt2	10.514546658	0.009175797
eca/Problem01_30_true.ll/4274.smt2	10.510418848	0.009999795
eca/Problem01_30_true.ll/5250.smt2	2.949805868	0.010022775
eca/Problem01_30_true.ll/5980.smt2	1.33225963	0.010806917
eca/Problem01_30_true.ll/5997.smt2	10.563029735	0.011751236
eca/Problem01_40_true.ll/2714.smt2	10.76221377	0.011697088
eca/Problem01_40_true.ll/4133.smt2	1.289538097	0.010894856
eca/Problem01_40_true.ll/4788.smt2	10.500708387	0.009303339
eca/Problem01_40_true.ll/5077.smt2	10.511877074	0.010298267
eca/Problem01_40_true.ll/5713.smt2	1.307025676	0.010794308
eca/Problem01_50_false.ll/2000.smt2	2.913873275	0.011640363
eca/Problem01_50_false.ll/2512.smt2	1.304078414	0.011768945
eca/Problem01_50_false.ll/4224.smt2	1.31880982	0.012284742
eca/Problem01_50_false.ll/4791.smt2	10.641876854	0.011768989
eca/Problem01_50_false.ll/5756.smt2	10.51656242	0.01200365
eca/Problem02_00_true.ll/1123.smt2	3.900621162	0.01781777
eca/Problem02_00_true.ll/1249.smt2	35.250222903	0.019921011
eca/Problem02_00_true.ll/2032.smt2	900	0.031141215
eca/Problem02_00_true.ll/2848.smt2	900	0.027416747
eca/Problem02_00_true.ll/2928.smt2	79.648313426	0.023678828
eca/Problem02_00_true.ll/3115.smt2	900	25.05332152
eca/Problem02_00_true.ll/3768.smt2	900	0.027534461
eca/Problem02_00_true.ll/3827.smt2	900	0.027967481
eca/Problem02_00_true.ll/4273.smt2	900	0.162674478
eca/Problem02_00_true.ll/4480.smt2	2.398446268	0.027642337
eca/Problem02_00_true.ll/4851.smt2	900	0.052523983
eca/Problem02_00_true.ll/783.smt2	13.477116421	0.019539135
eca/Problem02_00_true.ll/914.smt2	3.747783956	0.019607503
eca/Problem02_00_true.ll/998.smt2	14.028712083	0.019855284
eca/Problem02_10_true.ll/1171.smt2	13.491520439	0.019990857
eca/Problem02_10_true.ll/2183.smt2	176.497481221	0.023664197
eca/Problem02_10_true.ll/2440.smt2	900	0.031865668
eca/Problem02_10_true.ll/2508.smt2	900	0.027489513
eca/Problem02_10_true.ll/2721.smt2	900	0.751881347
eca/Problem02_10_true.ll/2763.smt2	900	24.734006938
eca/Problem02_10_true.ll/3254.smt2	125.756234127	0.030356541
eca/Problem02_10_true.ll/3458.smt2	0.607699511	0.026157997
eca/Problem02_10_true.ll/3596.smt2	900	0.103983901
eca/Problem02_10_true.ll/3744.smt2	900	0.026073958
eca/Problem02_10_true.ll/4452.smt2	900	0.043273741
eca/Problem02_10_true.ll/4774.smt2	900	0.042889906
eca/Problem02_20_true.ll/1310.smt2	1.643046144	0.023412599
eca/Problem02_20_true.ll/1593.smt2	34.979161373	0.01927005
eca/Problem02_20_true.ll/2119.smt2	900	0.027838859
eca/Problem02_20_true.ll/3087.smt2	8.273994585	0.027844851
eca/Problem02_20_true.ll/3265.smt2	900	0.745679537
eca/Problem02_20_true.ll/3277.smt2	79.186086757	0.021958611
eca/Problem02_20_true.ll/3749.smt2	0.813127538	0.027348572
eca/Problem02_20_true.ll/3778.smt2	900	64.789707591
eca/Problem02_20_true.ll/3873.smt2	900	65.276121676
eca/Problem02_20_true.ll/4619.smt2	900	0.044920032
eca/Problem02_20_true.ll/819.smt2	13.524574058	0.018675627
eca/Problem02_30_true.ll/1144.smt2	35.063283474	0.026466461
eca/Problem02_30_true.ll/1296.smt2	13.444386129	0.018619204
eca/Problem02_30_true.ll/1746.smt2	1.452638747	0.02207243
eca/Problem02_30_true.ll/2046.smt2	15.006503085	0.01959245
eca/Problem02_30_true.ll/2068.smt2	900	0.031922139
eca/Problem02_30_true.ll/2616.smt2	900	0.030472439
eca/Problem02_30_true.ll/2826.smt2	900	0.031070393
eca/Problem02_30_true.ll/3526.smt2	900	0.756208628
eca/Problem02_30_true.ll/3613.smt2	900	0.03299674
eca/Problem02_30_true.ll/3780.smt2	900	0.155324321
eca/Problem02_30_true.ll/3865.smt2	900	0.798103379
eca/Problem02_30_true.ll/4271.smt2	41.337922324	0.025534597
eca/Problem02_30_true.ll/4615.smt2	900	0.042809566
eca/Problem02_30_true.ll/550.smt2	1.649205434	0.017090987
eca/Problem02_40_true.ll/1486.smt2	3.748135106	0.018628223
eca/Problem02_40_true.ll/2046.smt2	15.122819164	0.01855362
eca/Problem02_40_true.ll/2146.smt2	900	0.02948472
eca/Problem02_40_true.ll/2434.smt2	900	0.755019432
eca/Problem02_40_true.ll/2471.smt2	900	0.386619786
eca/Problem02_40_true.ll/2528.smt2	900	0.027542604
eca/Problem02_40_true.ll/2888.smt2	900	0.034644674
eca/Problem02_40_true.ll/3090.smt2	900	0.751837863
eca/Problem02_40_true.ll/3138.smt2	900	0.388278337
eca/Problem02_40_true.ll/3154.smt2	900	0.38506228
eca/Problem02_40_true.ll/3805.smt2	0.820038319	0.026045201
eca/Problem02_40_true.ll/4032.smt2	900	1.363497366
eca/Problem02_40_true.ll/4060.smt2	900	64.735393853
eca/Problem02_50_false.ll/1041.smt2	35.210746217	0.020015211
eca/Problem02_50_false.ll/1108.smt2	1.64014086	0.018421571
eca/Problem02_50_false.ll/1837.smt2	175.983102471	0.023230146
eca/Problem02_50_false.ll/2205.smt2	177.41132992	0.024015073
eca/Problem02_50_false.ll/2787.smt2	900	0.391030885
eca/Problem02_50_false.ll/3479.smt2	900	0.032009886
eca/Problem02_50_false.ll/3480.smt2	900	0.103133704
eca/Problem02_50_false.ll/734.smt2	1.653737756	0.019755184
eca/Problem02_50_false.ll/996.smt2	1.654614773	0.025089889
eca/Problem02_60_false.ll/1053.smt2	13.645801956	0.01846031
eca/Problem02_60_false.ll/2104.smt2	177.256513397	0.025645152
eca/Problem02_60_false.ll/2157.smt2	15.017454803	0.023210204
eca/Problem02_60_false.ll/2388.smt2	900	0.073216122
eca/Problem02_60_false.ll/3165.smt2	900	0.028841125
eca/Problem02_60_false.ll/4005.smt2	900	0.040704334
eca/Problem02_60_false.ll/4044.smt2	1.00059312	0.02578701
eca/Problem02_60_false.ll/4054.smt2	900	0.035938021
eca/Problem02_60_false.ll/4619.smt2	900	0.04581247
eca/Problem02_60_false.ll/4989.smt2	900	0.217542797
eca/Problem02_60_false.ll/5015.smt2	900	0.045881993
eca/Problem02_60_false.ll/601.smt2	1.641188978	0.019263707
eca/Problem03_00_true.ll/1427.smt2	900	0.011433353
eca/Problem03_00_true.ll/1914.smt2	900	0.009364669
eca/Problem03_00_true.ll/3207.smt2	900	0.015663341
eca/Problem03_00_true.ll/3620.smt2	900	0.012544554
eca/Problem03_00_true.ll/4264.smt2	900	0.013100366
eca/Problem03_00_true.ll/4608.smt2	900	0.013380145
eca/Problem03_00_true.ll/4750.smt2	900	0.011904335
eca/Problem03_00_true.ll/5438.smt2	900	0.009245781
eca/Problem03_00_true.ll/5986.smt2	900	0.009515243
eca/Problem03_00_true.ll/6084.smt2	900	0.009756294
eca/Problem03_10_true.ll/2874.smt2	900	0.00964823
eca/Problem03_10_true.ll/3413.smt2	900	0.008659375
eca/Problem03_10_true.ll/4791.smt2	900	0.011533444
eca/Problem03_10_true.ll/937.smt2	26.304455605	0.011160331
eca/Problem03_20_true.ll/1320.smt2	27.249383317	0.011384061
eca/Problem03_20_true.ll/1406.smt2	27.129409575	0.012488242
eca/Problem03_20_true.ll/2478.smt2	900	0.008831987
eca/Problem03_20_true.ll/3447.smt2	900	0.01196124
eca/Problem03_20_true.ll/3762.smt2	900	0.009185076
eca/Problem03_20_true.ll/4374.smt2	900	0.009028636
eca/Problem03_20_true.ll/4440.smt2	900	0.012892282
eca/Problem03_20_true.ll/4494.smt2	900	0.011928937
eca/Problem03_20_true.ll/4508.smt2	900	0.011927679
eca/Problem03_20_true.ll/5203.smt2	900	0.0114498
eca/Problem03_30_true.ll/1435.smt2	900	0.011598354
eca/Problem03_30_true.ll/1976.smt2	63.175435303	0.009016557
eca/Problem03_30_true.ll/2126.smt2	900	0.008791711
eca/Problem03_30_true.ll/2409.smt2	900	0.010966602
eca/Problem03_30_true.ll/2521.smt2	132.05187947	0.009794792
eca/Problem03_30_true.ll/4445.smt2	900	0.009168971
eca/Problem03_30_true.ll/4657.smt2	900	0.012002123
eca/Problem03_30_true.ll/4708.smt2	900	0.011119132
eca/Problem03_30_true.ll/4894.smt2	900	0.01115918
eca/Problem03_30_true.ll/5316.smt2	900	0.012814496
eca/Problem03_30_true.ll/5318.smt2	900	0.013706879
eca/Problem03_40_true.ll/1840.smt2	900	0.010603828
eca/Problem03_40_true.ll/2667.smt2	133.891628852	0.01130551
eca/Problem03_40_true.ll/4255.smt2	900	0.010071275
eca/Problem03_40_true.ll/4507.smt2	900	0.009383418
eca/Problem03_40_true.ll/4657.smt2	900	0.012000376
eca/Problem03_40_true.ll/6042.smt2	900	0.011865225
eca/Problem03_50_false.ll/1321.smt2	26.756687733	0.008791009
eca/Problem03_50_false.ll/2306.smt2	900	0.014052092
eca/Problem03_50_false.ll/2439.smt2	900	0.012286895
eca/Problem03_50_false.ll/2470.smt2	900	0.01146959
eca/Problem03_50_false.ll/3034.smt2	900	0.009718745
eca/Problem03_50_false.ll/3570.smt2	900	0.011901222
eca/Problem03_50_false.ll/3663.smt2	900	0.007818293
eca/Problem03_50_false.ll/4448.smt2	900	0.012010752
eca/Problem03_50_false.ll/5110.smt2	900	0.009033294
eca/Problem03_50_false.ll/5288.smt2	900	0.00983375
eca/Problem03_50_false.ll/5433.smt2	900	0.011615097
eca/Problem04_00_true.ll/2497.smt2	2.961973406	0.007951463
eca/Problem04_00_true.ll/2537.smt2	2.890132326	0.010482509
eca/Problem04_00_true.ll/2557.smt2	2.903018599	0.007974303
eca/Problem04_00_true.ll/2707.smt2	2.929665117	0.00800649
eca/Problem04_40_false.ll/2557.smt2	2.922802353	0.009547668
eca/Problem04_50_true.ll/2722.smt2	2.878949699	0.0101959
eca/Problem10_00_true.ll/1094.smt2	900	0.047253441
eca/Problem10_00_true.ll/143.smt2	1.403932954	0.019493698
eca/Problem10_00_true.ll/245.smt2	900	0.023575388
eca/Problem10_00_true.ll/2490.smt2	900	0.047857168
eca/Problem10_00_true.ll/2627.smt2	900	0.034796622
eca/Problem10_00_true.ll/312.smt2	900	0.031977256
eca/Problem10_00_true.ll/4123.smt2	900	3.009846706
eca/Problem10_00_true.ll/4208.smt2	900	3.090645403
eca/Problem10_00_true.ll/4442.smt2	900	3.017346502
eca/Problem10_00_true.ll/4524.smt2	900	0.188056832
eca/Problem10_00_true.ll/477.smt2	900	0.032024533
eca/Problem10_00_true.ll/605.smt2	900	0.047989589
eca/Problem10_10_true.ll/1014.smt2	900	0.033379734
eca/Problem10_10_true.ll/1031.smt2	900	0.031887472
eca/Problem10_10_true.ll/1195.smt2	900	0.0331601
eca/Problem10_10_true.ll/1371.smt2	900	0.188720996
eca/Problem10_10_true.ll/1498.smt2	900	0.033703813
eca/Problem10_10_true.ll/1630.smt2	900	0.086884826
eca/Problem10_10_true.ll/1873.smt2	900	0.206818783
eca/Problem10_10_true.ll/210.smt2	900	0.023864001
eca/Problem10_10_true.ll/236.smt2	900	0.030805133
eca/Problem10_10_true.ll/2564.smt2	900	0.086466433
eca/Problem10_10_true.ll/2724.smt2	900	0.193874273
eca/Problem10_10_true.ll/2743.smt2	900	0.047729905
eca/Problem10_10_true.ll/3154.smt2	900	0.048028996
eca/Problem10_10_true.ll/3896.smt2	900	0.189228736
eca/Problem10_10_true.ll/4587.smt2	900	0.050202431
eca/Problem10_10_true.ll/4660.smt2	900	0.047965498
eca/Problem10_10_true.ll/4704.smt2	900	0.048797059
eca/Problem10_10_true.ll/477.smt2	900	0.028472148
eca/Problem10_10_true.ll/641.smt2	900	0.050355232
eca/Problem10_10_true.ll/772.smt2	900	0.03226825
eca/Problem10_20_true.ll/1193.smt2	900	0.087830937
eca/Problem10_20_true.ll/1230.smt2	900	0.085477939
eca/Problem10_20_true.ll/1366.smt2	900	0.189307498
eca/Problem10_20_true.ll/1456.smt2	900	0.08742504
eca/Problem10_20_true.ll/1508.smt2	900	0.089296519
eca/Problem10_20_true.ll/1854.smt2	900	0.030935484
eca/Problem10_20_true.ll/1936.smt2	900	0.035947633
eca/Problem10_20_true.ll/2069.smt2	900	0.047152373
eca/Problem10_20_true.ll/2641.smt2	900	0.090941649
eca/Problem10_20_true.ll/2892.smt2	900	0.191590481
eca/Problem10_20_true.ll/3074.smt2	900	0.047792443
eca/Problem10_20_true.ll/4029.smt2	900	0.387711911
eca/Problem10_20_true.ll/486.smt2	900	0.023101073
eca/Problem10_20_true.ll/607.smt2	900	0.049607611
eca/Problem10_20_true.ll/756.smt2	900	0.031973687
eca/Problem10_20_true.ll/763.smt2	900	0.033608382
eca/Problem10_20_true.ll/932.smt2	900	0.049106191
eca/Problem10_30_false.ll/1164.smt2	900	0.088244893
eca/Problem10_30_false.ll/1188.smt2	900	0.087387859
eca/Problem10_30_false.ll/158.smt2	900	0.023800025
eca/Problem10_30_false.ll/174.smt2	900	0.022662934
eca/Problem10_30_false.ll/2051.smt2	900	0.048457541
eca/Problem10_30_false.ll/2265.smt2	900	0.047427609
eca/Problem10_30_false.ll/2506.smt2	900	0.049829327
eca/Problem10_30_false.ll/2857.smt2	900	0.187800796
eca/Problem10_30_false.ll/320.smt2	900	0.036181721
eca/Problem10_30_false.ll/33.smt2	34.753360053	0.019559133
eca/Problem10_30_false.ll/4626.smt2	900	0.188612208
eca/Problem10_30_false.ll/4737.smt2	900	0.187895645
eca/Problem10_30_false.ll/4861.smt2	900	0.187123509
eca/Problem10_30_false.ll/606.smt2	900	0.032552328
eca/Problem10_40_false.ll/1294.smt2	900	0.19261674
eca/Problem10_40_false.ll/1356.smt2	900	0.048244851
eca/Problem10_40_false.ll/1419.smt2	900	0.048498455
eca/Problem10_40_false.ll/1612.smt2	900	0.208111926
eca/Problem10_40_false.ll/2655.smt2	900	0.087807427
eca/Problem10_40_false.ll/2751.smt2	900	0.089008192
eca/Problem10_40_false.ll/3107.smt2	900	0.205868098
eca/Problem10_40_false.ll/3666.smt2	900	0.447287172
eca/Problem10_40_false.ll/4509.smt2	900	0.048036705
eca/Problem10_40_false.ll/456.smt2	900	0.031614365
eca/Problem10_40_false.ll/4591.smt2	900	1.175848388
eca/Problem10_40_false.ll/462.smt2	900	0.034756176
eca/Problem10_40_false.ll/4727.smt2	900	0.18965509
eca/Problem10_40_false.ll/4855.smt2	900	0.186096478
eca/Problem10_40_false.ll/4891.smt2	900	0.189634446
eca/Problem10_40_false.ll/830.smt2	900	0.0479502
eca/Problem10_40_false.ll/937.smt2	900	0.047512349
eca/Problem10_50_false.ll/1050.smt2	900	0.047897579
eca/Problem10_50_false.ll/1637.smt2	900	0.086539049
eca/Problem10_50_false.ll/1773.smt2	900	0.031452336
eca/Problem10_50_false.ll/2233.smt2	900	0.18735573
eca/Problem10_50_false.ll/2618.smt2	900	0.087464131
eca/Problem10_50_false.ll/2753.smt2	900	0.205393569
eca/Problem10_50_false.ll/3303.smt2	900	1.153246882
eca/Problem10_50_false.ll/373.smt2	900	0.0259069
eca/Problem10_50_false.ll/3877.smt2	900	6.127274246
eca/Problem10_50_false.ll/3936.smt2	900	1.159144848
eca/Problem10_50_false.ll/4447.smt2	900	1.156589791
eca/Problem10_50_false.ll/4734.smt2	900	0.184106428
eca/Problem10_60_false.ll/1047.smt2	900	0.086358592
eca/Problem10_60_false.ll/1118.smt2	900	0.088046552
eca/Problem10_60_false.ll/1252.smt2	900	0.047539233
eca/Problem10_60_false.ll/202.smt2	900	0.02410863
eca/Problem10_60_false.ll/2682.smt2	900	0.087126541
eca/Problem10_60_false.ll/2839.smt2	900	0.203290114
eca/Problem10_60_false.ll/3266.smt2	900	0.186559933
eca/Problem10_60_false.ll/33.smt2	35.084744872	0.015831839
eca/Problem10_60_false.ll/344.smt2	900	0.024863136
eca/Problem10_60_false.ll/3895.smt2	900	2.996546246
eca/Problem10_60_false.ll/4061.smt2	900	1.180800926
eca/Problem10_60_false.ll/4540.smt2	900	0.392139891
eca/Problem10_60_false.ll/459.smt2	900	0.034295627
eca/Problem10_60_false.ll/4702.smt2	900	0.186120428
eca/Problem10_60_false.ll/55.smt2	0.804302025	0.018092975
eca/Problem11_10_false.ll/5290.smt2	2.953107084	0.011292701
eca/Problem11_30_false.ll/4488.smt2	10.624285161	0.01934471
eca/Problem11_30_false.ll/6278.smt2	10.579986511	0.010761889
eca/Problem11_40_false.ll/4044.smt2	1.359754977	0.011895111
eca/Problem11_40_false.ll/4199.smt2	1.27628665	0.01256334
eca/Problem11_40_false.ll/5063.smt2	1.282551941	0.011724289
eca/Problem11_40_false.ll/5549.smt2	10.565226739	0.015880435
eca/Problem11_40_false.ll/6730.smt2	2.957779564	0.012025858
eca/Problem11_50_false.ll/4612.smt2	1.276501314	0.015728646
eca/Problem11_50_false.ll/6542.smt2	0.612016908	0.011799392
eca/Problem11_60_false.ll/1862.smt2	0.512479761	0.011503946
eca/Problem11_60_false.ll/4961.smt2	2.93773041	0.011042952
eca/Problem11_60_false.ll/5103.smt2	5.914799997	0.011310899
eca/Problem11_60_false.ll/5528.smt2	2.914155642	0.012024873
eca/Problem11_60_false.ll/6796.smt2	6.015593033	0.011466227
eca/Problem13_10_false.ll/2608.smt2	0.559338888	0.013585976
eca/Problem13_20_false.ll/2552.smt2	0.577597383	0.014543091
eca/Problem13_30_false.ll/2482.smt2	0.558681336	0.014001044
eca/Problem14_00_true.ll/2628.smt2	1.255519168	0.012641529
eca/Problem14_00_true.ll/3339.smt2	1.255604798	0.014285721
eca/Problem14_00_true.ll/4418.smt2	10.566335434	0.011913676
eca/Problem14_00_true.ll/5040.smt2	26.732342885	0.017062663
eca/Problem14_00_true.ll/5367.smt2	10.349166444	0.015824969
eca/Problem14_10_false.ll/3294.smt2	26.404001961	0.01177057
eca/Problem14_10_false.ll/3462.smt2	10.392644771	0.011814095
eca/Problem14_10_false.ll/3498.smt2	10.41671569	0.010090059
eca/Problem14_10_false.ll/4851.smt2	1.284709604	0.011385366
eca/Problem14_20_true.ll/2309.smt2	2.921103609	0.011851776
eca/Problem14_20_true.ll/3128.smt2	10.47117671	0.012626164
eca/Problem14_20_true.ll/3924.smt2	10.456588363	0.015853177
eca/Problem14_20_true.ll/4781.smt2	10.451040633	0.011587171
eca/Problem14_20_true.ll/5122.smt2	10.558696225	0.012001907
eca/Problem14_20_true.ll/5654.smt2	1.279131813	0.011871701
eca/Problem14_20_true.ll/5939.smt2	10.807156846	0.01565324
eca/Problem14_30_true.ll/2496.smt2	1.275311478	0.011300005
eca/Problem14_30_true.ll/4456.smt2	26.353182843	0.015414665
eca/Problem14_40_false.ll/2623.smt2	1.288172348	0.011515252
eca/Problem14_40_false.ll/3591.smt2	10.459104539	0.012638855
eca/Problem14_40_false.ll/4068.smt2	26.652824989	0.015467385
eca/Problem14_40_false.ll/4153.smt2	10.353395308	0.012245442
eca/Problem14_40_false.ll/5163.smt2	10.514232892	0.01488505
eca/Problem14_40_false.ll/5289.smt2	10.514908642	0.01245644
eca/Problem14_40_false.ll/5556.smt2	2.895918818	0.013776359
eca/Problem14_40_false.ll/5965.smt2	10.578421308	0.01561829
eca/Problem14_50_true.ll/2622.smt2	1.286271888	0.013787731
eca/Problem14_50_true.ll/3250.smt2	10.397194976	0.011687491
eca/Problem14_50_true.ll/3937.smt2	26.287308962	0.011911728
eca/Problem14_50_true.ll/4562.smt2	1.281129804	0.011906762
eca/Problem14_50_true.ll/5760.smt2	1.288483954	0.010494057
eca/Problem14_50_true.ll/5793.smt2	1.278869242	0.01188046
eca/Problem14_50_true.ll/5927.smt2	10.461574366	0.013143798
eca/Problem16_00_false.ll/3705.smt2	1.257228205	0.012668869
eca/Problem16_00_false.ll/4309.smt2	1.263435984	0.012690052
eca/Problem16_08_false.ll/3105.smt2	1.279985684	0.013427347
eca/Problem16_08_false.ll/3404.smt2	1.280635682	0.012116087
eca/Problem16_08_false.ll/3623.smt2	1.283975061	0.012870512
eca/Problem16_08_false.ll/3944.smt2	1.280515051	0.012871131
eca/Problem16_20_false.ll/3454.smt2	1.272242178	0.01548505
eca/Problem16_20_false.ll/3690.smt2	1.292511051	0.015885386
eca/Problem16_20_false.ll/3779.smt2	1.279652576	0.011116584
eca/Problem16_20_false.ll/3794.smt2	1.268441214	0.01153212
eca/Problem16_40_false.ll/4066.smt2	10.419669792	0.010680304
eca/Problem17_30_false.ll/2564.smt2	2.877535041	0.011519921
eca/Problem17_30_false.ll/3060.smt2	26.660651272	0.01111245
eca/Problem17_50_false.ll/2692.smt2	2.900223703	0.012449441
eca/Problem17_50_false.ll/2713.smt2	2.904119146	0.01123369
eca/Problem17_50_false.ll/3057.smt2	900	0.011448289
eca/Problem17_50_false.ll/3105.smt2	900	0.013679046
eca/Problem17_50_false.ll/3724.smt2	0.612253994	0.015154226
eca/Problem17_50_false.ll/4112.smt2	0.596260067	0.012634328
eca/Problem17_60_false.ll/2641.smt2	2.898600827	0.010003849
eca/Problem17_60_false.ll/3253.smt2	2.916352478	0.012025911
ssh-simplified/s3_srvr_1_true.cil.ll/2784.smt2	0.943375868	0.018575135
ssh-simplified/s3_srvr_1_true.cil.ll/3422.smt2	1.194292478	0.01859032
ssh-simplified/s3_srvr_11_false.cil.ll/1261.smt2	1.628124646	0.025020507
ssh-simplified/s3_srvr_11_false.cil.ll/2632.smt2	0.730847415	0.059595893
ssh-simplified/s3_srvr_11_false.cil.ll/929.smt2	0.787143063	0.039357659
ssh-simplified/s3_srvr_2_true.cil.ll/1000.smt2	0.926762971	0.015886715
ssh-simplified/s3_srvr_2_true.cil.ll/597.smt2	0.623008829	0.019565718
ssh-simplified/s3_srvr_2_true.cil.ll/827.smt2	0.954653839	0.015316797
ssh-simplified/s3_srvr_2_true.cil.ll/998.smt2	0.884038065	0.019420884

2 Q3B

2.1 SMT-LIB

2.1.1 Load the results

First, lets get the data and merge them.

simplTimes <- read.csv("simpltimes_smtlib.csv", header=TRUE, stringsAsFactors=FALSE)
smtlib.q3b <- read.csv("q3b_smtlib.csv", header=TRUE, stringsAsFactors=FALSE)
smtlib.q3b_u <- read.csv("q3b_smtlib_unconstrained.csv", header=TRUE, stringsAsFactors=FALSE)

smtlib <- Reduce(function(x, y) merge(x, y, all=TRUE, by="filename"), list(smtlib.q3b, smtlib.q3b_u, simplTimes))
colnames(smtlib) = c('filename', 'result', 'cputime', 'walltime', 'memusage', 'result.u', 'cputime.u', 'walltime.u', 'memusage.u', 'simpltime')

smtlib$cputime[smtlib$result != "sat" & smtlib$result != "unsat"] <- 900
smtlib$walltime[smtlib$result != "sat" & smtlib$result != "unsat"] <- 900
smtlib$cputime.u[smtlib$result.u != "sat" & smtlib$result.u != "unsat"] <- 900
smtlib$walltime.u[smtlib$result.u != "sat" & smtlib$result.u != "unsat"] <- 900

Now, compare number of results of each type for each configuration.

smtlib_standard <- count(smtlib.q3b, "result")
colnames(smtlib_standard) <- c('result', 'standard')

smtlib_unconstrained <- count(smtlib.q3b_u, "result")
colnames(smtlib_unconstrained) <- c('result', 'unconstrained')

Reduce(function(...) merge(..., all=TRUE),
         list(smtlib_standard, smtlib_unconstrained))

result	standard	unconstrained
sat	94	94
timeout	3	3
unsat	94	94

2.1.2 Result counts

This table shows numbers of benchmarks grouped by the result in both of the configurations.

count(smtlib, c('result', 'result.u'))

result	result.u	freq
sat	sat	94
timeout	timeout	3
unsat	unsat	94

2.1.3 Total time/memory

Now, lets see the total CPU time, wall time, memory used and simplification times for both of the configurations.

numcolwise(sum)(smtlib[which((smtlib$result == "sat" & smtlib$result.u == "sat") | (smtlib$result == "unsat" & smtlib$result.u == "unsat")),])

cputime	walltime	memusage	cputime.u	walltime.u	memusage.u	simpltime
2986.159773999	1007.06066016108	nil	2233.902792755	756.874632652849	nil	15.6483904724009

2.1.4 Scatter plots

Linear scale

ggplot(smtlib, aes(cputime, cputime.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained", xlim=c(0.001,900), ylim=c(0.001,900)) +
  geom_point() +
  geom_abline(intercept=0) +
  theme(legend.title=element_blank())

Log scale

ggplot(smtlib, aes(cputime, cputime.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained", xlim=c(0.001,900), ylim=c(0.001,900)) +
  geom_point() +
  geom_abline(intercept=0) +
  scale_x_log10(breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  theme(legend.title=element_blank())

Log scale + simplification time

ggplot(smtlib, aes(cputime, cputime.u+simpltime, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained", xlim=c(0.001,900), ylim=c(0.001,900)) +
  geom_point() +
  geom_abline(intercept=0) +
  scale_x_log10(breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  theme(legend.title=element_blank())

Memory

ggplot(smtlib, aes(memusage, memusage.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained", xlim=c(1000000,8000000000), ylim=c(1000000,8000000000)) +
  geom_point() +
  geom_abline(intercept=0) +
  scale_x_log10(breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  theme(legend.title=element_blank())

2.1.5 Quantile plot

smtlib.ordered = sort(smtlib$cputime[smtlib$result == "sat" | smtlib$result == "unsat"]);
smtlib.ordered.u = sort(smtlib$cputime.u[smtlib$result.u == "sat" | smtlib$result.u == "unsat"]);
smtlib.ordered.us = sort((smtlib$cputime.u + smtlib$simpltime)[smtlib$result.u == "sat" | smtlib$result.u == "unsat"]);

plot(c(0, 195), c(0.01, 900), log='y', xlab=NA, ylab=NA, axes=FALSE, frame.plot=TRUE, type='n')

axis(1, at=seq(0,200,50), tck = -.01, label=NA)
axis(2, at=c(0.01,0.1,1,10,100), tck = -.01, label=NA)
axis(1, at=seq(0,200,50), lwd = 0, line = -.8)
axis(2, at=c(0.01,0.1,1,10,100), labels=c(0.01,0.1,1,10,100), lwd = 0, line = -.4, las = 1)

lines(1:length(smtlib.ordered), smtlib.ordered, type='s', col='blue')
lines(1:length(smtlib.ordered.u), smtlib.ordered.u, type='s', col='darkgreen')
lines(1:length(smtlib.ordered.us), smtlib.ordered.us, type='s', col='red')

mtext(side = 1, "formulas from SMT-LIB solved by Q3B", line = 1.2)
mtext(side = 2, "CPU time (s)", line = 2)

legend("topleft",
  lty=c(1,1,1),
  lwd=c(2.5,2.5,2.5),
  col=c("blue", "darkgreen", "red"),
  legend=c("standard", "unconstrained", "unconstrained+simplification time"))

2.1.6 Degraded performance

These are the results where the simplifications increase the solving time by more than 0.5 s.

smtlib[smtlib$cputime + 0.5 < smtlib$cputime.u, c('filename', 'cputime', 'cputime.u')]

filename	cputime	cputime.u
fixpoint/893180/sdlx-fixpoint-8.smt2	200.37546317	212.218630023
ranking/893007/audio_ac97_rtstream.cpp.smt2	16.972568783	19.29756979
ranking/893008/network_ndis_coisdn_TpiParam.c.smt2	17.591544933	19.121582216
ranking/893016/audio_ac97_wavepcistream.cpp.smt2	532.362251004	599.225281145
ranking/893032/network_ndis_rtlnwifi_extsta_st_misc.c.smt2	216.299660053	236.490280765
ranking/893051/hid_firefly_app_firefly.cpp.smt2	13.14870131	16.653695454

2.1.7 Improved performance

These are the results where the simplifications decrease the solving time by more than 0.5 s.

smtlib[smtlib$cputime.u + 0.5 < smtlib$cputime, c('filename', 'cputime', 'cputime.u')]

filename	cputime	cputime.u
fixpoint/893083/small-pipeline-fixpoint-10.smt2	106.50458874	0.063530962
fixpoint/893088/sdlx-fixpoint-6.smt2	40.385224539	38.024472295
fixpoint/893099/small-pipeline-fixpoint-6.smt2	100.563702745	0.066146831
fixpoint/893103/sdlx-fixpoint-9.smt2	612.7759794	572.555491751
fixpoint/893105/small-pipeline-fixpoint-8.smt2	106.8876212	0.065699216
fixpoint/893108/small-pipeline-fixpoint-4.smt2	100.002966679	0.064759105
fixpoint/893135/small-pipeline-fixpoint-5.smt2	107.307632263	0.065790116
fixpoint/893145/small-pipeline-fixpoint-7.smt2	105.110806063	0.069722747
fixpoint/893171/small-pipeline-fixpoint-9.smt2	105.130491658	0.0612756
fixpoint/893191/sdlx-fixpoint-7.smt2	161.785258078	160.996707309
ranking/893018/filesys_cdfs_allocsup.c.smt2	147.603340171	119.599520147
ranking/893024/hid_hclient_ecdisp.c.smt2	28.075621572	17.060574969
ranking/893025/filesys_fastfat_cachesup.c.smt2	19.650140754	16.987439444
ranking/893027/audio_ac97_common.cpp.smt2	20.247900391	16.985402133
ranking/893033/1394diag_isochapi.c.smt2	28.187218884	20.181525446
ranking/893034/input_pnpi8042_moudep.c.smt2	29.04420114	19.876979356
ranking/893040/filesys_fastfat_easup.c.smt2	28.04481745	21.706395211
ranking/893044/network_ndis_rtlnwifi_extsta_st_aplst.c.smt2	21.880982002	19.763220808
ranking/893045/kmdf_osrusbfx2_exe_testapp.c.smt2	20.64244117	17.661815767
ranking/893057/audio_dmusuart_mpu.cpp.smt2	25.906643028	20.001864949
ranking/893065/kernel_uagp35_gart.c.smt2	24.601649762	19.578427607

2.2 SymDIVINE

2.2.1 Load the results

First, lets get the data and merge them.

simplTimes <- read.csv("simpltimes_symdivine.csv", header=TRUE, stringsAsFactors=FALSE)
symdivine.q3b <- read.csv("q3b_symdivine.csv", header=TRUE, stringsAsFactors=FALSE)
symdivine.q3b_u <- read.csv("q3b_symdivine_unconstrained.csv", header=TRUE, stringsAsFactors=FALSE)

symdivine <- Reduce(function(x, y) merge(x, y, all=TRUE, by="filename"), list(symdivine.q3b, symdivine.q3b_u, simplTimes))
colnames(symdivine) = c('filename', 'result', 'cputime', 'walltime', 'memusage', 'result.u', 'cputime.u', 'walltime.u', 'memusage.u', 'simpltime')

symdivine$cputime[symdivine$result != "sat" & symdivine$result != "unsat"] <- 900
symdivine$walltime[symdivine$result != "sat" & symdivine$result != "unsat"] <- 900
symdivine$cputime.u[symdivine$result.u != "sat" & symdivine$result.u != "unsat"] <- 900
symdivine$walltime.u[symdivine$result.u != "sat" & symdivine$result.u != "unsat"] <- 900

Now, compare number of results of each type for each configuration.

symdivine_standard <- count(symdivine.q3b, "result")
colnames(symdivine_standard) <- c('result', 'standard')

symdivine_unconstrained <- count(symdivine.q3b_u, "result")
colnames(symdivine_unconstrained) <- c('result', 'unconstrained')

Reduce(function(...) merge(..., all=TRUE),
         list(symdivine_standard, symdivine_unconstrained)) #, symdivine_localunconstrained))

result	standard	unconstrained
sat	1137	1137
timeout	122	122
unsat	4202	4202

2.2.2 Result counts

This table shows numbers of benchmarks grouped by the result in both of the configurations.

count(symdivine, c('result', 'result.u'))

result	result.u	freq
sat	sat	1137
timeout	timeout	122
unsat	unsat	4202

2.2.3 Total time/memory

Now, lets see the total CPU time, wall time, memory used and simplification times for both of the configurations.

numcolwise(sum)(symdivine[which((symdivine$result == "sat" & symdivine$result.u == "sat") | (symdivine$result == "unsat" & symdivine$result.u == "unsat")),])

cputime	walltime	memusage	cputime.u	walltime.u	memusage.u	simpltime
9045.80764213	3468.35683208704	nil	3082.464226678	1435.79995086417	nil	142.671166041633

2.2.4 Scatter plots

Linear scale

ggplot(symdivine, aes(cputime, cputime.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained", xlim=c(0,300), ylim=c(0,300)) +
  geom_point() +
  geom_abline(intercept=0) +
  theme(legend.title=element_blank())

Log scale

ggplot(symdivine, aes(cputime, cputime.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained", xlim=c(0.001,900), ylim=c(0.001,900)) +
  geom_point() +
  geom_abline(intercept=0) +
  scale_x_log10(breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  theme(legend.title=element_blank())

Log scale + simplification time

          ggplot(symdivine, aes(cputime, cputime.u+simpltime, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory")
)), xlab = "Standard", ylab = "Unconstrained") +
            geom_point() +
            geom_abline(intercept=0) +
            scale_x_log10(name="Q3B", limits = c(0.01, 901), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
            scale_y_log10(name="Q3B + simplificatons", limits = c(0.01, 901), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
            theme(legend.title=element_blank()) +
            scale_colour_brewer(palette = "Set1")

Memory

ggplot(symdivine, aes(memusage, memusage.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained", log="xy", xlim=c(1000000,8000000000), ylim=c(1000000,8000000000)) +
  geom_point() +
  geom_abline(intercept=0) +
  scale_x_log10(breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  theme(legend.title=element_blank())

2.2.5 Quantile plot

symdivine.ordered = sort(symdivine$cputime[symdivine$result == "sat" | symdivine$result == "unsat"]);
symdivine.ordered.u = sort(symdivine$cputime.u[symdivine$result.u == "sat" | symdivine$result.u == "unsat"]);
symdivine.ordered.us = sort((symdivine$cputime.u + symdivine$simpltime)[symdivine$result.u == "sat" | symdivine$result.u == "unsat"]);

plot(c(0, 5500), c(0.01, 900), log='y', xlab=NA, ylab=NA, axes=FALSE, frame.plot=TRUE, type='n')

axis(1, at=seq(0,5500,500), tck = -.01, label=NA)
axis(2, at=c(0.01,0.1,1,10,100), tck = -.01, label=NA)
axis(1, at=seq(0,5500,500), lwd = 0, line = -.8)
axis(2, at=c(0.01,0.1,1,10,100), labels=c(0.01,0.1,1,10,100), lwd = 0, line = -.4, las = 1)

lines(1:length(symdivine.ordered), symdivine.ordered, type='s', col='blue')
lines(1:length(symdivine.ordered.u), symdivine.ordered.u, type='s', col='darkgreen')
lines(1:length(symdivine.ordered.us), symdivine.ordered.us, type='s', col='red')

mtext(side = 1, "Formulas from SymDIVINE solved by Q3B", line = 1.2)
mtext(side = 2, "CPU time (s)", line = 2)

legend("topleft",
  lty=c(1,1,1),
  lwd=c(2.5,2.5,2.5),
  col=c("blue", "darkgreen", "red"),
  legend=c("standard", "unconstrained", "unconstrained+simplification time"))

2.2.6 Degraded performance

These are the results where the simplifications increase the solving time by more than 0.5 s.

symdivine[symdivine$cputime + 0.5 < symdivine$cputime.u, c('filename', 'cputime', 'cputime.u')]

filename	cputime	cputime.u
bitvector/gcd_2_true.ll/327.smt2	185.965475472	187.820405408
bitvector/gcd_3_true.ll/352.smt2	176.234244199	177.106712106
bitvector/jain_7_true.ll/35.smt2	217.3160147	252.636331023
bitvector/jain_7_true.ll/42.smt2	266.799128343	270.489087542
bitvector/soft_float_4_true.c.cil.ll/3638.smt2	6.760098122	8.945602742
bitvector/soft_float_4_true.c.cil.ll/3977.smt2	11.397139945	14.481815526
recursive/gcd01_true.ll/262.smt2	8.500974884	9.433748545
recursive/gcd01_true.ll/278.smt2	11.806544369	12.915009205

2.2.7 Improved performance

These are the results where the simplifications decrease the solving time by more than 0.5 s.

symdivine[symdivine$cputime.u + 0.5 < symdivine$cputime, c('filename', 'cputime', 'cputime.u')]

filename	cputime	cputime.u
bitvector/gcd_2_true.ll/169.smt2	200.830754553	200.316424529
bitvector/gcd_2_true.ll/176.smt2	203.231936966	202.501793128
bitvector/gcd_2_true.ll/346.smt2	196.297385368	194.0637851
bitvector/gcd_2_true.ll/350.smt2	194.123057122	193.386965297
bitvector/soft_float_4_true.c.cil.ll/3401.smt2	9.428399772	8.920470435
eca/Problem10_00_true.ll/4123.smt2	0.878179301	0.115900809
eca/Problem10_00_true.ll/4208.smt2	0.878443699	0.119100421
eca/Problem10_00_true.ll/4442.smt2	0.889333812	0.100803664
eca/Problem10_00_true.ll/4524.smt2	0.638179789	0.103182382
eca/Problem10_20_true.ll/4029.smt2	0.807903001	0.103170883
eca/Problem10_30_false.ll/4737.smt2	0.622552435	0.08427502
eca/Problem10_40_false.ll/3666.smt2	0.617744064	0.103611705
eca/Problem10_40_false.ll/4591.smt2	0.955882796	0.106491427
eca/Problem10_40_false.ll/4727.smt2	0.6365926	0.088393389
eca/Problem10_40_false.ll/4855.smt2	0.730307082	0.089662869
eca/Problem10_40_false.ll/4891.smt2	0.76110709	0.092331237
eca/Problem10_50_false.ll/3303.smt2	0.82523836	0.101110848
eca/Problem10_50_false.ll/3877.smt2	0.930552687	0.098297773
eca/Problem10_50_false.ll/3936.smt2	0.84328888	0.089922904
eca/Problem10_50_false.ll/4447.smt2	0.849580159	0.093162179
eca/Problem10_60_false.ll/3895.smt2	0.875785417	0.101615242
eca/Problem10_60_false.ll/4061.smt2	0.843527704	0.112283608
eca/Problem10_60_false.ll/4540.smt2	0.628020448	0.105961909
locks/test_locks_10_true.ll/10455.smt2	1.021409258	0.050852971
locks/test_locks_10_true.ll/11656.smt2	1.696539804	0.051035084
locks/test_locks_10_true.ll/12219.smt2	9.403874434	0.045594878
locks/test_locks_10_true.ll/1919.smt2	0.658316731	0.042175938
locks/test_locks_10_true.ll/3306.smt2	2.642649458	0.053904119
locks/test_locks_10_true.ll/4023.smt2	0.566682985	0.049475865
locks/test_locks_10_true.ll/4453.smt2	3.826813307	0.048881301
locks/test_locks_10_true.ll/5928.smt2	1.727228847	0.048311026
locks/test_locks_10_true.ll/5993.smt2	6.046635727	0.044752383
locks/test_locks_10_true.ll/6135.smt2	1.198168304	0.067322488
locks/test_locks_10_true.ll/6228.smt2	0.597391877	0.053940538
locks/test_locks_10_true.ll/6417.smt2	4.76331852	0.05298096
locks/test_locks_10_true.ll/6691.smt2	0.935947574	0.059252547
locks/test_locks_10_true.ll/7331.smt2	3.640342704	0.064768532
locks/test_locks_10_true.ll/7536.smt2	1.506894339	0.053287576
locks/test_locks_10_true.ll/7836.smt2	4.733143315	0.052839097
locks/test_locks_10_true.ll/8574.smt2	3.067617166	0.048437572
locks/test_locks_10_true.ll/8762.smt2	7.400996251	0.06357128
locks/test_locks_10_true.ll/9037.smt2	8.397428145	0.054657342
locks/test_locks_10_true.ll/9287.smt2	6.70916858	0.04430675
locks/test_locks_11_true.ll/11853.smt2	4.388098171	0.05299604
locks/test_locks_11_true.ll/1217.smt2	0.996689628	0.058015668
locks/test_locks_11_true.ll/12600.smt2	2.343781095	0.060500741
locks/test_locks_11_true.ll/13818.smt2	9.055733563	0.068306505
locks/test_locks_11_true.ll/14872.smt2	14.50639202	0.061887999
locks/test_locks_11_true.ll/1513.smt2	0.619044014	0.064243939
locks/test_locks_11_true.ll/1743.smt2	0.758752312	0.049542859
locks/test_locks_11_true.ll/2303.smt2	0.610434486	0.066763022
locks/test_locks_11_true.ll/2622.smt2	2.485796839	0.057830197
locks/test_locks_11_true.ll/4774.smt2	0.743022768	0.063126426
locks/test_locks_11_true.ll/5971.smt2	4.336406059	0.060038836
locks/test_locks_11_true.ll/6014.smt2	0.781052164	0.042529461
locks/test_locks_11_true.ll/6045.smt2	2.187664255	0.064085893
locks/test_locks_11_true.ll/6204.smt2	5.409197429	0.052135517
locks/test_locks_11_true.ll/6397.smt2	3.412745554	0.069444056
locks/test_locks_11_true.ll/6659.smt2	5.908847819	0.048319571
locks/test_locks_11_true.ll/7519.smt2	0.855856725	0.061381271
locks/test_locks_11_true.ll/8248.smt2	7.636805381	0.049751147
locks/test_locks_11_true.ll/9281.smt2	6.282145569	0.055122221
locks/test_locks_11_true.ll/9313.smt2	9.172854662	0.047113217
locks/test_locks_11_true.ll/9366.smt2	2.617970409	0.063028159
locks/test_locks_12_true.ll/10839.smt2	7.123001488	0.056000775
locks/test_locks_12_true.ll/11546.smt2	4.228130934	0.049078743
locks/test_locks_12_true.ll/11783.smt2	0.710051801	0.049001734
locks/test_locks_12_true.ll/12158.smt2	4.180613249	0.050656805
locks/test_locks_12_true.ll/13906.smt2	2.82111671	0.060927452
locks/test_locks_12_true.ll/1474.smt2	1.12455867	0.050612068
locks/test_locks_12_true.ll/2105.smt2	0.583222759	0.051348411
locks/test_locks_12_true.ll/3268.smt2	0.821774132	0.046315417
locks/test_locks_12_true.ll/3453.smt2	1.7692721	0.055485481
locks/test_locks_12_true.ll/4502.smt2	1.329841093	0.050225411
locks/test_locks_12_true.ll/4614.smt2	2.16279909	0.047712209
locks/test_locks_12_true.ll/4878.smt2	0.972232632	0.052161303
locks/test_locks_12_true.ll/5930.smt2	1.81008146	0.048020351
locks/test_locks_12_true.ll/6768.smt2	5.46751867	0.047926679
locks/test_locks_12_true.ll/7342.smt2	4.37215135	0.052066964
locks/test_locks_12_true.ll/7479.smt2	5.58326874	0.052202216
locks/test_locks_12_true.ll/7866.smt2	7.198521625	0.055811342
locks/test_locks_12_true.ll/7926.smt2	2.464445604	0.046866756
locks/test_locks_12_true.ll/9094.smt2	2.530936303	0.044311708
locks/test_locks_12_true.ll/9229.smt2	2.548496899	0.065377362
locks/test_locks_12_true.ll/9875.smt2	0.644712906	0.061131576
locks/test_locks_12_true.ll/9940.smt2	4.008857484	0.055978795
locks/test_locks_13_true.ll/10099.smt2	2.088846993	0.047776427
locks/test_locks_13_true.ll/10340.smt2	4.542042075	0.071052227
locks/test_locks_13_true.ll/10643.smt2	4.473354067	0.056543725
locks/test_locks_13_true.ll/12306.smt2	1.853030536	0.056237525
locks/test_locks_13_true.ll/14039.smt2	2.783489604	0.061113176
locks/test_locks_13_true.ll/14400.smt2	3.105526913	0.050908935
locks/test_locks_13_true.ll/15757.smt2	3.668112344	0.055774175
locks/test_locks_13_true.ll/15975.smt2	1.661942731	0.062659854
locks/test_locks_13_true.ll/16642.smt2	3.373525251	0.060070583
locks/test_locks_13_true.ll/17851.smt2	5.457581454	0.050619601
locks/test_locks_13_true.ll/18068.smt2	2.117788322	0.052775636
locks/test_locks_13_true.ll/18346.smt2	2.614300869	0.060832467
locks/test_locks_13_true.ll/2320.smt2	0.889842394	0.059655879
locks/test_locks_13_true.ll/4039.smt2	0.968401768	0.046470928
locks/test_locks_13_true.ll/4588.smt2	2.294225394	0.057173795
locks/test_locks_13_true.ll/5472.smt2	0.83177352	0.058975526
locks/test_locks_13_true.ll/5939.smt2	1.522962253	0.052328407
locks/test_locks_13_true.ll/6474.smt2	0.951667244	0.046627938
locks/test_locks_13_true.ll/8183.smt2	1.257874793	0.053574004
locks/test_locks_13_true.ll/9390.smt2	1.104855351	0.048511839
locks/test_locks_14_true.ll/10372.smt2	4.431479228	0.050707578
locks/test_locks_14_true.ll/10717.smt2	9.396021548	0.049140402
locks/test_locks_14_true.ll/10810.smt2	4.745197787	0.062762609
locks/test_locks_14_true.ll/11846.smt2	3.923394492	0.064921675
locks/test_locks_14_true.ll/11977.smt2	2.454992939	0.047285329
locks/test_locks_14_true.ll/12446.smt2	2.567258304	0.049280812
locks/test_locks_14_true.ll/13733.smt2	2.409438524	0.049483253
locks/test_locks_14_true.ll/13786.smt2	6.099266768	0.060637485
locks/test_locks_14_true.ll/15419.smt2	1.611850577	0.064079718
locks/test_locks_14_true.ll/3937.smt2	0.660368968	0.053525946
locks/test_locks_14_true.ll/4733.smt2	3.54993416	0.052162283
locks/test_locks_14_true.ll/5555.smt2	4.940052309	0.050298434
locks/test_locks_14_true.ll/5593.smt2	1.078337317	0.048488247
locks/test_locks_14_true.ll/5716.smt2	1.84638586	0.049456718
locks/test_locks_14_true.ll/5844.smt2	3.096968439	0.049110792
locks/test_locks_14_true.ll/6403.smt2	3.737611635	0.060790026
locks/test_locks_14_true.ll/6549.smt2	6.179382024	0.054791664
locks/test_locks_14_true.ll/7845.smt2	5.424565036	0.059764849
locks/test_locks_14_true.ll/9107.smt2	3.321760328	0.059785195
locks/test_locks_14_true.ll/9533.smt2	4.607107115	0.066281416
locks/test_locks_14_true.ll/9656.smt2	3.623225486	0.065667638
locks/test_locks_15_true.ll/10125.smt2	7.470789119	0.067034598
locks/test_locks_15_true.ll/11153.smt2	8.973636427	0.051079883
locks/test_locks_15_true.ll/11176.smt2	0.637273618	0.05344522
locks/test_locks_15_true.ll/11203.smt2	1.643119009	0.051418037
locks/test_locks_15_true.ll/13343.smt2	10.818557451	0.05385576
locks/test_locks_15_true.ll/14253.smt2	3.663889374	0.044646804
locks/test_locks_15_true.ll/1801.smt2	0.742082478	0.046900447
locks/test_locks_15_true.ll/1980.smt2	0.643580015	0.058044218
locks/test_locks_15_true.ll/2472.smt2	1.951439213	0.058442676
locks/test_locks_15_true.ll/2551.smt2	2.498150307	0.045284614
locks/test_locks_15_true.ll/2824.smt2	1.630115363	0.045218104
locks/test_locks_15_true.ll/3059.smt2	2.029295533	0.048642138
locks/test_locks_15_true.ll/4153.smt2	2.320197876	0.041777934
locks/test_locks_15_true.ll/4692.smt2	1.310415204	0.055464677
locks/test_locks_15_true.ll/5850.smt2	3.489049318	0.055519588
locks/test_locks_15_true.ll/6481.smt2	1.752165907	0.053573536
locks/test_locks_15_true.ll/7222.smt2	4.342955171	0.059778769
locks/test_locks_15_true.ll/8170.smt2	2.027958428	0.049156868
locks/test_locks_15_true.ll/8426.smt2	2.002023084	0.048895105
locks/test_locks_5_true.ll/10086.smt2	4.352708253	0.055352956
locks/test_locks_5_true.ll/10635.smt2	2.757588313	0.045964643
locks/test_locks_5_true.ll/11680.smt2	3.014002796	0.062752198
locks/test_locks_5_true.ll/12173.smt2	5.236238525	0.04497656
locks/test_locks_5_true.ll/12296.smt2	2.958718323	0.04599046
locks/test_locks_5_true.ll/12511.smt2	7.421874105	0.054776113
locks/test_locks_5_true.ll/14257.smt2	3.950125548	0.051569618
locks/test_locks_5_true.ll/14709.smt2	0.91913308	0.043892518
locks/test_locks_5_true.ll/15281.smt2	3.697426781	0.044058594
locks/test_locks_5_true.ll/3400.smt2	3.411835167	0.0488207
locks/test_locks_5_true.ll/3762.smt2	0.642155742	0.044778965
locks/test_locks_5_true.ll/4035.smt2	0.977949229	0.044511989
locks/test_locks_5_true.ll/4038.smt2	1.113990976	0.048971219
locks/test_locks_5_true.ll/4583.smt2	0.780556636	0.051371118
locks/test_locks_5_true.ll/4626.smt2	2.888923288	0.054615889
locks/test_locks_5_true.ll/5418.smt2	2.770188997	0.054371339
locks/test_locks_5_true.ll/5518.smt2	2.531054321	0.050451192
locks/test_locks_5_true.ll/6898.smt2	6.713623695	0.049865408
locks/test_locks_5_true.ll/7606.smt2	6.013070333	0.04664221
locks/test_locks_5_true.ll/7616.smt2	6.895038364	0.046612652
locks/test_locks_5_true.ll/8289.smt2	1.582342594	0.044100957
locks/test_locks_5_true.ll/9122.smt2	4.325738405	0.047063077
locks/test_locks_5_true.ll/9607.smt2	1.005568206	0.057256771
locks/test_locks_5_true.ll/9954.smt2	5.007173357	0.055915696
locks/test_locks_6_true.ll/10096.smt2	5.066609865	0.058800401
locks/test_locks_6_true.ll/10110.smt2	6.181158244	0.048696788
locks/test_locks_6_true.ll/10679.smt2	5.889941936	0.046437792
locks/test_locks_6_true.ll/10775.smt2	2.423970315	0.046848432
locks/test_locks_6_true.ll/11449.smt2	8.682911368	0.052657095
locks/test_locks_6_true.ll/1318.smt2	1.103420898	0.050359253
locks/test_locks_6_true.ll/13517.smt2	12.125259928	0.072507209
locks/test_locks_6_true.ll/13748.smt2	3.305225237	0.061309301
locks/test_locks_6_true.ll/13981.smt2	8.804849066	0.049180211
locks/test_locks_6_true.ll/14374.smt2	1.120529297	0.043157627
locks/test_locks_6_true.ll/14598.smt2	4.155827189	0.057097428
locks/test_locks_6_true.ll/1526.smt2	1.056454844	0.051942158
locks/test_locks_6_true.ll/1752.smt2	1.098548673	0.064294003
locks/test_locks_6_true.ll/3071.smt2	2.731267552	0.068885241
locks/test_locks_6_true.ll/4134.smt2	1.360341694	0.056397803
locks/test_locks_6_true.ll/4203.smt2	0.566654667	0.060713531
locks/test_locks_6_true.ll/5444.smt2	4.422812336	0.057641481
locks/test_locks_6_true.ll/5590.smt2	0.95945481	0.05763588
locks/test_locks_6_true.ll/5982.smt2	5.129880549	0.04812204
locks/test_locks_6_true.ll/7046.smt2	1.109696438	0.065111652
locks/test_locks_6_true.ll/8869.smt2	5.30158576	0.064425525
locks/test_locks_7_true.ll/10564.smt2	8.509100291	0.073216165
locks/test_locks_7_true.ll/11210.smt2	1.993968297	0.063314276
locks/test_locks_7_true.ll/12398.smt2	12.012480461	0.054936002
locks/test_locks_7_true.ll/13959.smt2	6.753663879	0.046986608
locks/test_locks_7_true.ll/13992.smt2	9.942644662	0.063621953
locks/test_locks_7_true.ll/14010.smt2	11.963510113	0.049757429
locks/test_locks_7_true.ll/14076.smt2	3.039305754	0.048007528
locks/test_locks_7_true.ll/14964.smt2	5.896745046	0.05287362
locks/test_locks_7_true.ll/3814.smt2	3.146537686	0.069335498
locks/test_locks_7_true.ll/4795.smt2	1.59026987	0.04914061
locks/test_locks_7_true.ll/5168.smt2	0.651744503	0.06561154
locks/test_locks_7_true.ll/6498.smt2	2.634592149	0.052678863
locks/test_locks_7_true.ll/6782.smt2	6.573310843	0.060528638
locks/test_locks_7_true.ll/7996.smt2	7.680947992	0.064397042
locks/test_locks_7_true.ll/8460.smt2	4.095994938	0.069153069
locks/test_locks_7_true.ll/8925.smt2	0.872158843	0.058779398
locks/test_locks_7_true.ll/9223.smt2	2.198598017	0.067695984
locks/test_locks_7_true.ll/9526.smt2	4.106545687	0.048436677
locks/test_locks_7_true.ll/9553.smt2	6.125850059	0.049382446
locks/test_locks_8_true.ll/10864.smt2	9.488025201	0.054668241
locks/test_locks_8_true.ll/11791.smt2	0.965967426	0.047737621
locks/test_locks_8_true.ll/12801.smt2	5.160975595	0.047819893
locks/test_locks_8_true.ll/12972.smt2	6.082254431	0.047046224
locks/test_locks_8_true.ll/13137.smt2	6.455685377	0.060051213
locks/test_locks_8_true.ll/13493.smt2	9.449574657	0.062774607
locks/test_locks_8_true.ll/14143.smt2	8.325011278	0.062990221
locks/test_locks_8_true.ll/15152.smt2	7.206072416	0.048420602
locks/test_locks_8_true.ll/15351.smt2	9.66708358	0.051301315
locks/test_locks_8_true.ll/2540.smt2	1.905843009	0.067082959
locks/test_locks_8_true.ll/3202.smt2	1.38246758	0.050245619
locks/test_locks_8_true.ll/4076.smt2	3.097046047	0.066057351
locks/test_locks_8_true.ll/5036.smt2	4.203024081	0.050045482
locks/test_locks_8_true.ll/5242.smt2	4.625187829	0.047621053
locks/test_locks_8_true.ll/5845.smt2	3.186498512	0.054196457
locks/test_locks_8_true.ll/8438.smt2	2.68097444	0.066589519
locks/test_locks_8_true.ll/8683.smt2	1.809582058	0.054786418
locks/test_locks_8_true.ll/9807.smt2	4.458006636	0.058248533
locks/test_locks_8_true.ll/9810.smt2	4.662540518	0.05530408
locks/test_locks_9_true.ll/10112.smt2	6.331113139	0.054316459
locks/test_locks_9_true.ll/10465.smt2	1.429931819	0.052050965
locks/test_locks_9_true.ll/11097.smt2	4.226271982	0.050530405
locks/test_locks_9_true.ll/11130.smt2	6.785576453	0.04922118
locks/test_locks_9_true.ll/11312.smt2	10.095327409	0.054246958
locks/test_locks_9_true.ll/11730.smt2	6.721877213	0.051344702
locks/test_locks_9_true.ll/11960.smt2	1.571308808	0.047030227
locks/test_locks_9_true.ll/13903.smt2	2.649527725	0.048076912
locks/test_locks_9_true.ll/14259.smt2	4.121098108	0.052674596
locks/test_locks_9_true.ll/15009.smt2	10.188073075	0.04717128
locks/test_locks_9_true.ll/2250.smt2	1.108048734	0.049767323
locks/test_locks_9_true.ll/4969.smt2	0.686396317	0.048325242
locks/test_locks_9_true.ll/5525.smt2	3.02427156	0.068455561
locks/test_locks_9_true.ll/7476.smt2	5.393244267	0.05579848
locks/test_locks_9_true.ll/7578.smt2	3.948498926	0.05743141
locks/test_locks_9_true.ll/7650.smt2	1.110571077	0.051061154
locks/test_locks_9_true.ll/7914.smt2	1.83722387	0.056608474
locks/test_locks_9_true.ll/7925.smt2	2.427921491	0.055330394
locks/test_locks_9_true.ll/8228.smt2	5.894727105	0.055219167
locks/test_locks_9_true.ll/9272.smt2	5.433207304	0.044864885
recursive/gcd01_true.ll/190.smt2	78.720898198	76.536689956
ssh-simplified/s3_srvr_1_true.cil.ll/2031.smt2	1.031041525	0.06507418
ssh-simplified/s3_srvr_1_true.cil.ll/2098.smt2	1.472569056	0.06633518
ssh-simplified/s3_srvr_1_true.cil.ll/2784.smt2	2.038501153	0.056851338
ssh-simplified/s3_srvr_1_true.cil.ll/2813.smt2	0.954756872	0.075048912
ssh-simplified/s3_srvr_1_true.cil.ll/2826.smt2	0.773851499	0.071858888
ssh-simplified/s3_srvr_1_true.cil.ll/2901.smt2	2.340660711	0.058824323
ssh-simplified/s3_srvr_1_true.cil.ll/3081.smt2	0.595269789	0.052575824
ssh-simplified/s3_srvr_1_true.cil.ll/3422.smt2	2.325973811	0.061965812
ssh-simplified/s3_srvr_1_true.cil.ll/3485.smt2	1.958133338	0.070689693
ssh-simplified/s3_srvr_11_false.cil.ll/1071.smt2	3.73977476	0.115389798
ssh-simplified/s3_srvr_11_false.cil.ll/1261.smt2	3.944268859	0.123825148
ssh-simplified/s3_srvr_11_false.cil.ll/1731.smt2	3.203600967	0.092074033
ssh-simplified/s3_srvr_11_false.cil.ll/1754.smt2	7.282406231	0.216036724
ssh-simplified/s3_srvr_11_false.cil.ll/1944.smt2	6.364848882	0.186452559
ssh-simplified/s3_srvr_11_false.cil.ll/2039.smt2	4.031276347	0.135576072
ssh-simplified/s3_srvr_11_false.cil.ll/2040.smt2	1.27874209	0.049183253
ssh-simplified/s3_srvr_11_false.cil.ll/2143.smt2	2.675293656	0.084690976
ssh-simplified/s3_srvr_11_false.cil.ll/2262.smt2	1.608784875	0.087857912
ssh-simplified/s3_srvr_11_false.cil.ll/2294.smt2	7.541406282	0.200230009
ssh-simplified/s3_srvr_11_false.cil.ll/2510.smt2	1.646804882	0.057984102
ssh-simplified/s3_srvr_11_false.cil.ll/2632.smt2	8.64635567	0.26965791
ssh-simplified/s3_srvr_11_false.cil.ll/395.smt2	0.668055699	0.087856225
ssh-simplified/s3_srvr_11_false.cil.ll/471.smt2	0.807761224	0.076003369
ssh-simplified/s3_srvr_11_false.cil.ll/827.smt2	0.772311715	0.054393301
ssh-simplified/s3_srvr_11_false.cil.ll/852.smt2	2.506417196	0.078030246
ssh-simplified/s3_srvr_11_false.cil.ll/861.smt2	0.62295314	0.055274597
ssh-simplified/s3_srvr_11_false.cil.ll/929.smt2	1.28669371	0.090102341
ssh-simplified/s3_srvr_12_false.cil.ll/10139.smt2	5.555201593	0.053956057
ssh-simplified/s3_srvr_12_false.cil.ll/11393.smt2	3.185296054	0.056039828
ssh-simplified/s3_srvr_12_false.cil.ll/11433.smt2	6.533966156	0.06002178
ssh-simplified/s3_srvr_12_false.cil.ll/2851.smt2	0.726692614	0.061174891
ssh-simplified/s3_srvr_12_false.cil.ll/3360.smt2	0.804503884	0.054087001
ssh-simplified/s3_srvr_12_false.cil.ll/3828.smt2	0.606501975	0.053796966
ssh-simplified/s3_srvr_12_false.cil.ll/4313.smt2	0.67857832	0.063330345
ssh-simplified/s3_srvr_12_false.cil.ll/4769.smt2	1.008536972	0.060556088
ssh-simplified/s3_srvr_12_false.cil.ll/5771.smt2	1.788960809	0.059367709
ssh-simplified/s3_srvr_12_false.cil.ll/6221.smt2	0.763918347	0.052647112
ssh-simplified/s3_srvr_12_false.cil.ll/6258.smt2	1.160902783	0.059428213
ssh-simplified/s3_srvr_12_false.cil.ll/7428.smt2	1.242419597	0.059651223
ssh-simplified/s3_srvr_12_false.cil.ll/7451.smt2	1.73276623	0.055879985
ssh-simplified/s3_srvr_12_false.cil.ll/8170.smt2	5.36386325	0.052059094
ssh-simplified/s3_srvr_12_false.cil.ll/8688.smt2	1.958726242	0.057455444
ssh-simplified/s3_srvr_12_false.cil.ll/8721.smt2	5.200271445	0.06082366
ssh-simplified/s3_srvr_12_false.cil.ll/9205.smt2	1.072446661	0.060986165
ssh-simplified/s3_srvr_12_false.cil.ll/9412.smt2	5.233378211	0.068230109
ssh-simplified/s3_srvr_12_false.cil.ll/9805.smt2	2.07159125	0.052649632
ssh-simplified/s3_srvr_12_false.cil.ll/9875.smt2	1.040430003	0.051731245
ssh-simplified/s3_srvr_13_false.cil.ll/1109.smt2	1.407997949	0.112002537
ssh-simplified/s3_srvr_13_false.cil.ll/1186.smt2	2.471598639	0.093445651
ssh-simplified/s3_srvr_13_false.cil.ll/1502.smt2	1.293683983	0.102375088
ssh-simplified/s3_srvr_13_false.cil.ll/1612.smt2	2.538341794	0.100227226
ssh-simplified/s3_srvr_13_false.cil.ll/1625.smt2	0.659162623	0.068860419
ssh-simplified/s3_srvr_13_false.cil.ll/1839.smt2	1.330037233	0.110892372
ssh-simplified/s3_srvr_13_false.cil.ll/1868.smt2	2.393702434	0.081439455
ssh-simplified/s3_srvr_13_false.cil.ll/2080.smt2	1.472259782	0.100525753
ssh-simplified/s3_srvr_13_false.cil.ll/269.smt2	1.346507246	0.100635439
ssh-simplified/s3_srvr_13_false.cil.ll/2735.smt2	1.467222229	0.103084955
ssh-simplified/s3_srvr_13_false.cil.ll/2937.smt2	1.348176291	0.095895123
ssh-simplified/s3_srvr_13_false.cil.ll/3202.smt2	1.408770553	0.070372454
ssh-simplified/s3_srvr_13_false.cil.ll/3282.smt2	1.15056127	0.096268685
ssh-simplified/s3_srvr_13_false.cil.ll/343.smt2	2.327179084	0.093530385
ssh-simplified/s3_srvr_13_false.cil.ll/3692.smt2	1.415312731	0.10108887
ssh-simplified/s3_srvr_13_false.cil.ll/4118.smt2	1.308845291	0.10712648
ssh-simplified/s3_srvr_13_false.cil.ll/432.smt2	1.310547145	0.104027326
ssh-simplified/s3_srvr_13_false.cil.ll/4622.smt2	1.346451368	0.098110173
ssh-simplified/s3_srvr_13_false.cil.ll/4886.smt2	1.275086294	0.09194565
ssh-simplified/s3_srvr_13_false.cil.ll/5064.smt2	2.179170998	0.080575121
ssh-simplified/s3_srvr_13_false.cil.ll/5113.smt2	1.21721835	0.119179725
ssh-simplified/s3_srvr_13_false.cil.ll/5115.smt2	1.205852973	0.115432103
ssh-simplified/s3_srvr_13_false.cil.ll/5507.smt2	2.483686034	0.100238578
ssh-simplified/s3_srvr_13_false.cil.ll/553.smt2	1.308266396	0.103830343
ssh-simplified/s3_srvr_13_false.cil.ll/661.smt2	1.314684115	0.09607299
ssh-simplified/s3_srvr_1b_true.cil.ll/10159.smt2	1.98433955	0.062053783
ssh-simplified/s3_srvr_1b_true.cil.ll/13602.smt2	1.632515308	0.046709118
ssh-simplified/s3_srvr_1b_true.cil.ll/13986.smt2	1.959007306	0.046145879
ssh-simplified/s3_srvr_1b_true.cil.ll/15389.smt2	1.527650193	0.061981672
ssh-simplified/s3_srvr_1b_true.cil.ll/15616.smt2	0.936628419	0.05058838
ssh-simplified/s3_srvr_1b_true.cil.ll/17270.smt2	2.892866773	0.055416565
ssh-simplified/s3_srvr_1b_true.cil.ll/18192.smt2	3.493196084	0.049871111
ssh-simplified/s3_srvr_1b_true.cil.ll/20530.smt2	3.815973131	0.052155129
ssh-simplified/s3_srvr_1b_true.cil.ll/5322.smt2	1.101271783	0.054540642
ssh-simplified/s3_srvr_1b_true.cil.ll/8197.smt2	0.796655934	0.052980555
ssh-simplified/s3_srvr_1b_true.cil.ll/8929.smt2	0.704729815	0.052698295
ssh-simplified/s3_srvr_1b_true.cil.ll/9710.smt2	1.485802092	0.058187569
ssh-simplified/s3_srvr_2_false.cil.ll/341.smt2	0.648484521	0.064286238
ssh-simplified/s3_srvr_2_false.cil.ll/361.smt2	0.57739532	0.052367046
ssh-simplified/s3_srvr_2_false.cil.ll/563.smt2	0.643439137	0.064756423
ssh-simplified/s3_srvr_2_true.cil.ll/1000.smt2	1.803051069	0.062445017
ssh-simplified/s3_srvr_2_true.cil.ll/597.smt2	0.990712246	0.061041383
ssh-simplified/s3_srvr_2_true.cil.ll/827.smt2	1.794027024	0.053379538
ssh-simplified/s3_srvr_2_true.cil.ll/832.smt2	0.612249298	0.06811635
ssh-simplified/s3_srvr_2_true.cil.ll/853.smt2	1.165092249	0.074714367
ssh-simplified/s3_srvr_2_true.cil.ll/860.smt2	1.896172054	0.074541049
ssh-simplified/s3_srvr_2_true.cil.ll/945.smt2	0.573551265	0.05792852
ssh-simplified/s3_srvr_2_true.cil.ll/998.smt2	1.660596725	0.053601135
ssh-simplified/s3_srvr_3_true.cil.ll/285.smt2	0.612059039	0.059750096
ssh-simplified/s3_srvr_7_true.cil.ll/201.smt2	0.557456487	0.052810641
ssh-simplified/s3_srvr_7_true.cil.ll/287.smt2	0.723051276	0.059481741
ssh-simplified/s3_srvr_7_true.cil.ll/308.smt2	0.790744549	0.042940811
ssh-simplified/s3_srvr_7_true.cil.ll/309.smt2	0.830581308	0.050439712
ssh-simplified/s3_srvr_7_true.cil.ll/352.smt2	0.594406434	0.05295953
ssh-simplified/s3_srvr_8_true.cil.ll/612.smt2	0.59162161	0.064030695
ssh-simplified/s3_srvr_8_true.cil.ll/689.smt2	0.673023871	0.0646465
systemc/pc_sfifo_1_true.cil.ll/1101.smt2	133.866369781	0.053117204
systemc/pc_sfifo_1_true.cil.ll/123.smt2	2.154345735	0.045837717
systemc/pc_sfifo_1_true.cil.ll/129.smt2	2.173627754	0.075878387
systemc/pc_sfifo_1_true.cil.ll/138.smt2	2.197063994	0.062598639
systemc/pc_sfifo_1_true.cil.ll/209.smt2	2.152855305	0.055284335
systemc/pc_sfifo_1_true.cil.ll/212.smt2	2.242314321	0.048944129
systemc/pc_sfifo_1_true.cil.ll/270.smt2	4.347918197	0.05035777
systemc/pc_sfifo_1_true.cil.ll/304.smt2	5.501028038	0.062891068
systemc/pc_sfifo_1_true.cil.ll/386.smt2	14.225553146	0.053356341
systemc/pc_sfifo_1_true.cil.ll/418.smt2	17.526286832	0.047576071
systemc/pc_sfifo_1_true.cil.ll/420.smt2	17.460663143	0.056111228
systemc/pc_sfifo_1_true.cil.ll/458.smt2	24.69399673	0.053975914
systemc/pc_sfifo_1_true.cil.ll/479.smt2	27.163272227	0.051884973
systemc/pc_sfifo_1_true.cil.ll/486.smt2	28.304706033	0.052687115
systemc/pc_sfifo_1_true.cil.ll/587.smt2	43.593327618	0.053254499
systemc/pc_sfifo_1_true.cil.ll/588.smt2	43.576899638	0.052127981
systemc/pc_sfifo_1_true.cil.ll/655.smt2	50.235764001	0.05422997
systemc/pc_sfifo_1_true.cil.ll/709.smt2	56.116319441	0.057807955
systemc/pc_sfifo_1_true.cil.ll/735.smt2	55.065690908	0.059602382
systemc/pc_sfifo_1_true.cil.ll/769.smt2	61.754621764	0.0469175
systemc/pc_sfifo_1_true.cil.ll/784.smt2	61.655546916	0.054871827
systemc/pc_sfifo_1_true.cil.ll/795.smt2	65.03365702	0.052794238
systemc/pc_sfifo_1_true.cil.ll/818.smt2	69.943564357	0.066487934
systemc/pc_sfifo_1_true.cil.ll/871.smt2	75.394135351	0.056973821
systemc/pc_sfifo_2_true.cil.ll/1053.smt2	54.526865908	0.057389344
systemc/pc_sfifo_2_true.cil.ll/1181.smt2	69.016971883	0.048346785
systemc/pc_sfifo_2_true.cil.ll/1211.smt2	72.293320613	0.053397219
systemc/pc_sfifo_2_true.cil.ll/1348.smt2	90.775680026	0.0529309
systemc/pc_sfifo_2_true.cil.ll/1351.smt2	93.089096623	0.052999918
systemc/pc_sfifo_2_true.cil.ll/1452.smt2	102.340938422	0.051399419
systemc/pc_sfifo_2_true.cil.ll/146.smt2	2.068020172	0.051295057
systemc/pc_sfifo_2_true.cil.ll/178.smt2	2.208666218	0.063026978
systemc/pc_sfifo_2_true.cil.ll/206.smt2	2.252975956	0.063450291
systemc/pc_sfifo_2_true.cil.ll/250.smt2	2.205394397	0.04871981
systemc/pc_sfifo_2_true.cil.ll/256.smt2	2.203225991	0.04855544
systemc/pc_sfifo_2_true.cil.ll/267.smt2	2.46151286	0.05435493
systemc/pc_sfifo_2_true.cil.ll/345.smt2	4.109837409	0.052639638
systemc/pc_sfifo_2_true.cil.ll/354.smt2	4.391099508	0.048998817
systemc/pc_sfifo_2_true.cil.ll/463.smt2	10.509378432	0.054418297
systemc/pc_sfifo_2_true.cil.ll/571.smt2	17.416069291	0.067050946
systemc/pc_sfifo_2_true.cil.ll/669.smt2	27.180258189	0.052464099
systemc/pc_sfifo_2_true.cil.ll/752.smt2	32.98224607	0.053009762
systemc/pc_sfifo_2_true.cil.ll/772.smt2	34.579853935	0.059457075
systemc/pc_sfifo_2_true.cil.ll/793.smt2	34.461035257	0.057278749
systemc/pc_sfifo_2_true.cil.ll/865.smt2	43.114432414	0.051952786
systemc/pc_sfifo_2_true.cil.ll/952.smt2	49.757891222	0.055017915
systemc/pc_sfifo_2_true.cil.ll/996.smt2	52.50018983	0.051838022
systemc/pipeline_true.cil.ll/1015.smt2	1.207066	0.048644038
systemc/pipeline_true.cil.ll/1047.smt2	1.205007423	0.051049262
systemc/pipeline_true.cil.ll/1145.smt2	1.204810083	0.048417438
systemc/pipeline_true.cil.ll/156.smt2	1.194231554	0.057567877
systemc/pipeline_true.cil.ll/1594.smt2	1.192073863	0.057359192
systemc/pipeline_true.cil.ll/2291.smt2	1.246468665	0.0531037
systemc/pipeline_true.cil.ll/2819.smt2	1.20761234	0.050782326
systemc/pipeline_true.cil.ll/291.smt2	1.186764893	0.057055038
systemc/pipeline_true.cil.ll/3067.smt2	1.21062361	0.056723962
systemc/pipeline_true.cil.ll/3092.smt2	1.199324228	0.054418995
systemc/pipeline_true.cil.ll/3187.smt2	1.203818629	0.051640478
systemc/pipeline_true.cil.ll/4264.smt2	1.216235144	0.048472291
systemc/pipeline_true.cil.ll/4363.smt2	1.213026564	0.052331765
systemc/pipeline_true.cil.ll/4437.smt2	1.203224345	0.054692039
systemc/pipeline_true.cil.ll/4787.smt2	1.197950291	0.054788843
systemc/pipeline_true.cil.ll/4788.smt2	1.19976124	0.054721013
systemc/pipeline_true.cil.ll/5693.smt2	1.222742052	0.046727841
systemc/pipeline_true.cil.ll/6053.smt2	1.192473455	0.049347477
systemc/pipeline_true.cil.ll/6592.smt2	1.227594811	0.059514792
systemc/pipeline_true.cil.ll/6809.smt2	1.208201433	0.056610605
systemc/pipeline_true.cil.ll/7037.smt2	1.2252927	0.056218104
systemc/pipeline_true.cil.ll/7102.smt2	1.213333736	0.047655799
systemc/pipeline_true.cil.ll/7180.smt2	1.231044557	0.051511682
systemc/pipeline_true.cil.ll/7215.smt2	1.269882787	0.059492498
systemc/pipeline_true.cil.ll/7527.smt2	1.199899044	0.060052804
systemc/token_ring.01_false.cil.ll/2373.smt2	1.00904642	0.047611891
systemc/token_ring.01_false.cil.ll/3386.smt2	0.809098073	0.062720596
systemc/token_ring.01_false.cil.ll/4080.smt2	1.821691054	0.059984595
systemc/token_ring.01_false.cil.ll/5807.smt2	1.709327872	0.062376588
systemc/token_ring.01_false.cil.ll/6053.smt2	1.405709414	0.055480873
systemc/token_ring.01_false.cil.ll/6374.smt2	0.912022007	0.060339344
systemc/token_ring.01_false.cil.ll/6400.smt2	0.577742905	0.066798082
systemc/token_ring.01_false.cil.ll/6572.smt2	1.701104619	0.069775851
systemc/token_ring.01_false.cil.ll/6574.smt2	1.803971945	0.054320545
systemc/token_ring.01_false.cil.ll/6944.smt2	0.900200006	0.074583346
systemc/token_ring.01_false.cil.ll/7207.smt2	1.501199194	0.055507776
systemc/token_ring.01_true.cil.ll/2967.smt2	0.687555469	0.062444924
systemc/token_ring.01_true.cil.ll/3132.smt2	1.3557849	0.058895584
systemc/token_ring.01_true.cil.ll/3448.smt2	0.606503105	0.049689083
systemc/token_ring.01_true.cil.ll/4263.smt2	0.599873652	0.056057638
systemc/token_ring.01_true.cil.ll/4553.smt2	1.146618889	0.0597491
systemc/token_ring.01_true.cil.ll/5395.smt2	2.198200295	0.070593749
systemc/token_ring.01_true.cil.ll/5865.smt2	1.977017889	0.067531517
systemc/token_ring.01_true.cil.ll/6306.smt2	2.224000188	0.050159562
systemc/token_ring.01_true.cil.ll/6551.smt2	0.740020909	0.059856413
systemc/token_ring.01_true.cil.ll/6633.smt2	2.338247665	0.050946001
systemc/token_ring.01_true.cil.ll/7508.smt2	2.352885961	0.055117073
systemc/token_ring.01_true.cil.ll/7585.smt2	2.688480792	0.053562593
systemc/token_ring.01_true.cil.ll/8349.smt2	1.464980064	0.056667143
systemc/token_ring.02_false.cil.ll/2463.smt2	0.8224292	0.052361861
systemc/token_ring.02_false.cil.ll/3071.smt2	0.866587693	0.05304204
systemc/token_ring.02_false.cil.ll/3108.smt2	2.281049148	0.067376004
systemc/token_ring.02_false.cil.ll/3187.smt2	2.598688828	0.051329633
systemc/token_ring.02_false.cil.ll/3332.smt2	2.295908385	0.055785571
systemc/token_ring.02_false.cil.ll/3607.smt2	0.620487636	0.056424376
systemc/token_ring.02_false.cil.ll/4611.smt2	1.227906429	0.05652479
systemc/token_ring.02_false.cil.ll/4870.smt2	1.309873501	0.052763053
systemc/token_ring.02_false.cil.ll/5760.smt2	3.333028952	0.051160996
systemc/token_ring.02_false.cil.ll/5997.smt2	0.630771433	0.055676164
systemc/token_ring.02_true.cil.ll/1342.smt2	0.978893129	0.054210732
systemc/token_ring.02_true.cil.ll/1684.smt2	1.08989978	0.063853535
systemc/token_ring.02_true.cil.ll/3428.smt2	0.839608114	0.052748544
systemc/token_ring.02_true.cil.ll/3432.smt2	1.705437761	0.057638868
systemc/token_ring.02_true.cil.ll/3591.smt2	0.823515201	0.054317581
systemc/token_ring.02_true.cil.ll/4027.smt2	1.920933303	0.05517053
systemc/token_ring.02_true.cil.ll/5235.smt2	1.099085669	0.05245745
systemc/token_ring.02_true.cil.ll/5243.smt2	2.094466173	0.049258148
systemc/token_ring.02_true.cil.ll/5406.smt2	0.927864577	0.05576136
systemc/token_ring.02_true.cil.ll/5452.smt2	1.031968369	0.051195618
systemc/token_ring.02_true.cil.ll/5680.smt2	0.963599527	0.051591161
systemc/token_ring.02_true.cil.ll/5776.smt2	1.259949586	0.050228046
systemc/token_ring.02_true.cil.ll/5797.smt2	4.131223564	0.070548655
systemc/token_ring.02_true.cil.ll/5907.smt2	2.138611004	0.070263716
systemc/token_ring.02_true.cil.ll/6124.smt2	3.101849754	0.05871575
systemc/token_ring.02_true.cil.ll/6298.smt2	2.690586778	0.051906715
systemc/token_ring.02_true.cil.ll/6761.smt2	1.021058543	0.062769444
systemc/token_ring.04_false.cil.ll/1253.smt2	2.042862068	0.067570066
systemc/token_ring.04_false.cil.ll/1540.smt2	0.842038057	0.066631606
systemc/token_ring.04_false.cil.ll/1561.smt2	1.661452418	0.064001414
systemc/token_ring.04_false.cil.ll/1798.smt2	0.660501325	0.057313787
systemc/token_ring.04_false.cil.ll/2089.smt2	1.978620452	0.06225559
systemc/token_ring.04_false.cil.ll/2493.smt2	1.880203973	0.056439599
systemc/token_ring.04_false.cil.ll/3023.smt2	3.090985176	0.060030532
systemc/token_ring.04_false.cil.ll/3318.smt2	3.222133244	0.065505311
systemc/token_ring.04_false.cil.ll/3569.smt2	4.035934424	0.057445545
systemc/token_ring.04_false.cil.ll/3712.smt2	1.057942548	0.054558397
systemc/token_ring.04_false.cil.ll/3750.smt2	2.31687463	0.061102139
systemc/token_ring.04_false.cil.ll/4470.smt2	1.506350925	0.058436061
systemc/token_ring.04_false.cil.ll/4600.smt2	4.850813935	0.055711508
systemc/token_ring.04_false.cil.ll/4992.smt2	0.695986208	0.065089168
systemc/token_ring.04_false.cil.ll/5003.smt2	5.852476649	0.071405762
systemc/token_ring.04_false.cil.ll/5271.smt2	0.758206576	0.070848019
systemc/token_ring.04_false.cil.ll/5306.smt2	0.848570362	0.058938013
systemc/token_ring.04_true.cil.ll/1227.smt2	1.113511575	0.0611613
systemc/token_ring.04_true.cil.ll/1856.smt2	1.902891691	0.05976846
systemc/token_ring.04_true.cil.ll/1981.smt2	0.986905678	0.070989926
systemc/token_ring.04_true.cil.ll/2083.smt2	0.709013657	0.060875398
systemc/token_ring.04_true.cil.ll/2183.smt2	1.787676557	0.058707078
systemc/token_ring.04_true.cil.ll/2817.smt2	2.619470295	0.063837381
systemc/token_ring.04_true.cil.ll/3445.smt2	2.602029402	0.053613149
systemc/token_ring.04_true.cil.ll/4092.smt2	1.057894798	0.058058323
systemc/token_ring.04_true.cil.ll/4139.smt2	1.593742862	0.052264917
systemc/token_ring.04_true.cil.ll/4452.smt2	0.875456402	0.052793826
systemc/token_ring.04_true.cil.ll/4988.smt2	2.800637613	0.066080298
systemc/token_ring.04_true.cil.ll/5502.smt2	4.098553886	0.06682911
systemc/token_ring.04_true.cil.ll/5826.smt2	1.993561385	0.057153849
systemc/token_ring.04_true.cil.ll/5843.smt2	0.724592804	0.051760815
systemc/token_ring.04_true.cil.ll/5891.smt2	4.778989148	0.064026571
systemc/token_ring.06_false.cil.ll/1246.smt2	2.176580759	0.060144317
systemc/token_ring.06_false.cil.ll/1533.smt2	0.920961961	0.058618667
systemc/token_ring.06_false.cil.ll/1700.smt2	3.316817026	0.070407491
systemc/token_ring.06_false.cil.ll/1750.smt2	2.648558865	0.05784678
systemc/token_ring.06_false.cil.ll/1952.smt2	1.720655303	0.057042779
systemc/token_ring.06_false.cil.ll/2083.smt2	2.060705066	0.069193125
systemc/token_ring.06_false.cil.ll/2092.smt2	2.059825039	0.05963033
systemc/token_ring.06_false.cil.ll/2123.smt2	2.036631677	0.06601775
systemc/token_ring.06_false.cil.ll/2171.smt2	3.737778693	0.05273659
systemc/token_ring.06_false.cil.ll/2216.smt2	0.704038975	0.065826841
systemc/token_ring.06_false.cil.ll/2233.smt2	3.024367355	0.061215775
systemc/token_ring.06_false.cil.ll/2353.smt2	3.115744375	0.053257734
systemc/token_ring.06_false.cil.ll/2554.smt2	0.644347993	0.050790884
systemc/token_ring.06_false.cil.ll/2619.smt2	4.247544369	0.060302319
systemc/token_ring.06_false.cil.ll/2685.smt2	0.898922967	0.051710179
systemc/token_ring.06_false.cil.ll/2720.smt2	0.698137198	0.051082795
systemc/token_ring.06_false.cil.ll/2737.smt2	2.159664656	0.056868605
systemc/token_ring.06_false.cil.ll/2861.smt2	3.637319196	0.07208575
systemc/token_ring.06_false.cil.ll/2986.smt2	0.89668777	0.058878237
systemc/token_ring.06_false.cil.ll/3386.smt2	5.985479523	0.050923858
systemc/token_ring.06_false.cil.ll/3721.smt2	4.339270233	0.060154749
systemc/token_ring.06_false.cil.ll/3958.smt2	2.899678728	0.058596157
systemc/token_ring.06_false.cil.ll/4217.smt2	7.014087037	0.061084063
systemc/token_ring.06_false.cil.ll/528.smt2	1.310529639	0.060927502
systemc/token_ring.06_true.cil.ll/1349.smt2	2.169556543	0.064724958
systemc/token_ring.06_true.cil.ll/1458.smt2	2.05404358	0.067003859
systemc/token_ring.06_true.cil.ll/1677.smt2	3.293715067	0.061331896
systemc/token_ring.06_true.cil.ll/1854.smt2	2.333946532	0.060941896
systemc/token_ring.06_true.cil.ll/1924.smt2	1.403218373	0.054423686
systemc/token_ring.06_true.cil.ll/2494.smt2	2.032919754	0.062534667
systemc/token_ring.06_true.cil.ll/2748.smt2	3.907533161	0.057545918
systemc/token_ring.06_true.cil.ll/2836.smt2	2.348652065	0.075530812
systemc/token_ring.06_true.cil.ll/2912.smt2	4.143336215	0.063670399
systemc/token_ring.06_true.cil.ll/3095.smt2	2.278154495	0.067458455
systemc/token_ring.06_true.cil.ll/3131.smt2	4.470302912	0.058228797
systemc/token_ring.06_true.cil.ll/3169.smt2	3.969254989	0.075272109
systemc/token_ring.06_true.cil.ll/3274.smt2	4.165653885	0.060999335
systemc/token_ring.06_true.cil.ll/3417.smt2	6.023580327	0.060237273
systemc/token_ring.06_true.cil.ll/3813.smt2	4.191401503	0.056635905
systemc/token_ring.06_true.cil.ll/485.smt2	1.550625763	0.05324737
systemc/token_ring.06_true.cil.ll/536.smt2	1.297506429	0.057295523
systemc/token_ring.06_true.cil.ll/543.smt2	1.018196366	0.058111071
systemc/token_ring.06_true.cil.ll/640.smt2	1.34275592	0.0572213
systemc/token_ring.06_true.cil.ll/705.smt2	1.679208473	0.07376696
systemc/token_ring.06_true.cil.ll/944.smt2	0.749593955	0.060703508
systemc/token_ring.10_false.cil.ll/1045.smt2	0.932918876	0.060684884
systemc/token_ring.10_false.cil.ll/1054.smt2	3.158587967	0.060412885
systemc/token_ring.10_false.cil.ll/1283.smt2	2.756015483	0.062225322
systemc/token_ring.10_false.cil.ll/1512.smt2	2.379103436	0.054747495
systemc/token_ring.10_false.cil.ll/1584.smt2	4.249453434	0.070436157
systemc/token_ring.10_false.cil.ll/1707.smt2	3.354275836	0.069353476
systemc/token_ring.10_false.cil.ll/1733.smt2	4.775065751	0.061241622
systemc/token_ring.10_false.cil.ll/1840.smt2	3.425119583	0.061085471
systemc/token_ring.10_false.cil.ll/1861.smt2	2.235457852	0.078731645
systemc/token_ring.10_false.cil.ll/1921.smt2	3.601577084	0.062403266
systemc/token_ring.10_false.cil.ll/1966.smt2	2.254443652	0.06524077
systemc/token_ring.10_false.cil.ll/1987.smt2	3.605313594	0.060851339
systemc/token_ring.10_false.cil.ll/2056.smt2	6.961636672	0.062912051
systemc/token_ring.10_false.cil.ll/2203.smt2	4.635579228	0.066320648
systemc/token_ring.10_false.cil.ll/3119.smt2	2.56645223	0.062062378
systemc/token_ring.10_false.cil.ll/3295.smt2	12.677828359	0.057716076
systemc/token_ring.10_false.cil.ll/3709.smt2	2.421072058	0.066290425
systemc/token_ring.10_false.cil.ll/3715.smt2	6.247687586	0.086661313
systemc/token_ring.10_false.cil.ll/3732.smt2	9.151502399	0.065485199
systemc/token_ring.10_false.cil.ll/3799.smt2	7.438191148	0.0602404
systemc/token_ring.10_false.cil.ll/541.smt2	2.200147964	0.065583283
systemc/token_ring.10_false.cil.ll/661.smt2	1.958432412	0.069007485
systemc/token_ring.10_false.cil.ll/737.smt2	2.116401832	0.072084288
systemc/token_ring.10_false.cil.ll/773.smt2	1.180897138	0.076605277
systemc/token_ring.10_false.cil.ll/844.smt2	1.222679438	0.072492634
systemc/token_ring.10_true.cil.ll/1175.smt2	1.710710514	0.061161112
systemc/token_ring.10_true.cil.ll/1292.smt2	2.128468492	0.057260428
systemc/token_ring.10_true.cil.ll/1429.smt2	3.162125933	0.060308619
systemc/token_ring.10_true.cil.ll/1438.smt2	1.925383834	0.061214664
systemc/token_ring.10_true.cil.ll/1922.smt2	3.597370711	0.06165385
systemc/token_ring.10_true.cil.ll/2126.smt2	4.575069739	0.055022161
systemc/token_ring.10_true.cil.ll/215.smt2	0.873960252	0.058521701
systemc/token_ring.10_true.cil.ll/2220.smt2	8.3503416	0.063722772
systemc/token_ring.10_true.cil.ll/2231.smt2	7.435548996	0.068070011
systemc/token_ring.10_true.cil.ll/2376.smt2	3.623365346	0.05775811
systemc/token_ring.10_true.cil.ll/2487.smt2	4.0302051	0.066385459
systemc/token_ring.10_true.cil.ll/2552.smt2	2.633345072	0.056444732
systemc/token_ring.10_true.cil.ll/2632.smt2	10.852786347	0.059401159
systemc/token_ring.10_true.cil.ll/2700.smt2	2.643016306	0.079212438
systemc/token_ring.10_true.cil.ll/2906.smt2	4.275325601	0.066171895
systemc/token_ring.10_true.cil.ll/2912.smt2	5.959680849	0.062120961
systemc/token_ring.10_true.cil.ll/2983.smt2	9.333660487	0.05529939
systemc/token_ring.10_true.cil.ll/3031.smt2	5.827956327	0.066796249
systemc/token_ring.10_true.cil.ll/3130.smt2	2.598854802	0.063484548
systemc/token_ring.10_true.cil.ll/319.smt2	0.886222051	0.063991811
systemc/token_ring.10_true.cil.ll/3594.smt2	4.340936046	0.069738228
systemc/token_ring.10_true.cil.ll/3713.smt2	4.571178093	0.063738538
systemc/token_ring.12_false.cil.ll/1017.smt2	1.797224669	0.059607799
systemc/token_ring.12_false.cil.ll/1201.smt2	0.82408557	0.066082304
systemc/token_ring.12_false.cil.ll/1319.smt2	3.703025568	0.059812018
systemc/token_ring.12_false.cil.ll/1567.smt2	2.003586064	0.057774926
systemc/token_ring.12_false.cil.ll/1855.smt2	2.001585216	0.066805127
systemc/token_ring.12_false.cil.ll/1953.smt2	3.311766608	0.065762526
systemc/token_ring.12_false.cil.ll/1986.smt2	5.593167902	0.069230577
systemc/token_ring.12_false.cil.ll/1989.smt2	5.554983685	0.062222435
systemc/token_ring.12_false.cil.ll/2009.smt2	2.438800915	0.06800658
systemc/token_ring.12_false.cil.ll/2272.smt2	4.249899318	0.063266015
systemc/token_ring.12_false.cil.ll/235.smt2	1.301930836	0.059073144
systemc/token_ring.12_false.cil.ll/2560.smt2	9.116471904	0.070270029
systemc/token_ring.12_false.cil.ll/2721.smt2	6.792050811	0.079229204
systemc/token_ring.12_false.cil.ll/2884.smt2	3.245006539	0.064662748
systemc/token_ring.12_false.cil.ll/3031.smt2	2.899206134	0.070856672
systemc/token_ring.12_false.cil.ll/3046.smt2	2.937981413	0.083405144
systemc/token_ring.12_false.cil.ll/3181.smt2	2.903766908	0.06145646
systemc/token_ring.12_false.cil.ll/3258.smt2	5.715014791	0.07929003
systemc/token_ring.12_false.cil.ll/3433.smt2	2.331835423	0.068887569
systemc/token_ring.12_false.cil.ll/3964.smt2	5.740556511	0.06671563
systemc/token_ring.12_false.cil.ll/3976.smt2	6.86603748	0.061833583
systemc/token_ring.12_false.cil.ll/3988.smt2	1.698833834	0.089745969
systemc/token_ring.12_false.cil.ll/516.smt2	1.460331881	0.061943332
systemc/token_ring.12_false.cil.ll/535.smt2	1.454116311	0.070590032
systemc/token_ring.12_false.cil.ll/564.smt2	1.440668548	0.061308821
systemc/token_ring.12_true.cil.ll/1103.smt2	1.802815836	0.07591955
systemc/token_ring.12_true.cil.ll/1181.smt2	0.961369585	0.06492099
systemc/token_ring.12_true.cil.ll/1303.smt2	1.507659752	0.073580206
systemc/token_ring.12_true.cil.ll/1435.smt2	0.763959454	0.073749179
systemc/token_ring.12_true.cil.ll/152.smt2	1.319750006	0.06602127
systemc/token_ring.12_true.cil.ll/1577.smt2	2.014101878	0.057137995
systemc/token_ring.12_true.cil.ll/1592.smt2	1.996718013	0.064139982
systemc/token_ring.12_true.cil.ll/1719.smt2	4.786982696	0.065134634
systemc/token_ring.12_true.cil.ll/1726.smt2	3.927797663	0.068422536
systemc/token_ring.12_true.cil.ll/1797.smt2	5.235340424	0.081872429
systemc/token_ring.12_true.cil.ll/1911.smt2	0.991568805	0.0683378
systemc/token_ring.12_true.cil.ll/1978.smt2	6.548863279	0.075650525
systemc/token_ring.12_true.cil.ll/2096.smt2	2.436258983	0.076062597
systemc/token_ring.12_true.cil.ll/2474.smt2	4.551654953	0.073816147
systemc/token_ring.12_true.cil.ll/2863.smt2	9.548262213	0.060795528
systemc/token_ring.12_true.cil.ll/2998.smt2	3.666146023	0.066974605
systemc/token_ring.12_true.cil.ll/3348.smt2	2.980401179	0.067050417
systemc/token_ring.12_true.cil.ll/3361.smt2	1.645592648	0.056448158
systemc/token_ring.12_true.cil.ll/3526.smt2	3.190418588	0.058030304
systemc/token_ring.12_true.cil.ll/3724.smt2	1.654677942	0.062441448
systemc/token_ring.12_true.cil.ll/804.smt2	2.861883821	0.058612527
systemc/token_ring.12_true.cil.ll/95.smt2	0.709718871	0.070734806
systemc/token_ring.12_true.cil.ll/985.smt2	1.625274281	0.07044006
systemc/token_ring.14_false.cil.ll/1233.smt2	4.24729718	0.061656525
systemc/token_ring.14_false.cil.ll/1286.smt2	3.630360498	0.062950143
systemc/token_ring.14_false.cil.ll/1304.smt2	1.505755718	0.077474182
systemc/token_ring.14_false.cil.ll/1422.smt2	3.32515339	0.061686824
systemc/token_ring.14_false.cil.ll/1570.smt2	2.013111931	0.061929441
systemc/token_ring.14_false.cil.ll/1833.smt2	6.319039058	0.06309543
systemc/token_ring.14_false.cil.ll/1910.smt2	1.520647914	0.076868509
systemc/token_ring.14_false.cil.ll/2013.smt2	2.429670602	0.076767008
systemc/token_ring.14_false.cil.ll/2042.smt2	5.969916808	0.06840414
systemc/token_ring.14_false.cil.ll/2078.smt2	2.44490271	0.059572213
systemc/token_ring.14_false.cil.ll/2082.smt2	2.428137764	0.08103105
systemc/token_ring.14_false.cil.ll/2208.smt2	4.27703728	0.067370913
systemc/token_ring.14_false.cil.ll/2679.smt2	8.370276797	0.07179644
systemc/token_ring.14_false.cil.ll/2685.smt2	8.482067369	0.075197103
systemc/token_ring.14_false.cil.ll/2802.smt2	3.076853484	0.064601486
systemc/token_ring.14_false.cil.ll/3130.smt2	2.927818929	0.083523595
systemc/token_ring.14_false.cil.ll/3187.smt2	2.947101903	0.069716808
systemc/token_ring.14_false.cil.ll/3264.smt2	1.62881352	0.090528291
systemc/token_ring.14_false.cil.ll/3291.smt2	12.109736484	0.06574843
systemc/token_ring.14_false.cil.ll/383.smt2	1.086333105	0.064903172
systemc/token_ring.14_false.cil.ll/408.smt2	0.611300531	0.07304029
systemc/token_ring.14_false.cil.ll/554.smt2	1.475727881	0.065095654
systemc/token_ring.14_false.cil.ll/721.smt2	1.503986078	0.060903171
systemc/token_ring.14_false.cil.ll/751.smt2	2.034452006	0.065124757
systemc/toy_true.cil.ll/1016.smt2	168.397860643	0.068589037
systemc/toy_true.cil.ll/1037.smt2	176.800372218	0.066945025
systemc/toy_true.cil.ll/1049.smt2	177.364329388	0.063399624
systemc/toy_true.cil.ll/1052.smt2	181.615712926	0.062301052
systemc/toy_true.cil.ll/1091.smt2	163.816214979	0.065013628
systemc/toy_true.cil.ll/1171.smt2	186.232865233	0.063652849
systemc/toy_true.cil.ll/1289.smt2	221.619959863	0.060500828
systemc/toy_true.cil.ll/166.smt2	1.900745915	0.050001534
systemc/toy_true.cil.ll/203.smt2	1.866217834	0.065342087
systemc/toy_true.cil.ll/288.smt2	5.613229819	0.061675805
systemc/toy_true.cil.ll/346.smt2	12.339130111	0.065224742
systemc/toy_true.cil.ll/480.smt2	36.944650562	0.052116159
systemc/toy_true.cil.ll/546.smt2	43.701987129	0.049918918
systemc/toy_true.cil.ll/563.smt2	44.880417642	0.051628768
systemc/toy_true.cil.ll/601.smt2	53.130068992	0.057876249
systemc/toy_true.cil.ll/641.smt2	61.442464677	0.049759969
systemc/toy_true.cil.ll/736.smt2	84.336255935	0.051971981
systemc/toy_true.cil.ll/771.smt2	84.931189633	0.071024674
systemc/toy_true.cil.ll/820.smt2	83.504711145	0.065714473
systemc/toy_true.cil.ll/832.smt2	86.964354569	0.052522558
systemc/toy_true.cil.ll/843.smt2	96.185524188	0.050600058
systemc/toy_true.cil.ll/856.smt2	96.808963904	0.055551622
systemc/toy_true.cil.ll/911.smt2	122.735342823	0.051450746
systemc/toy_true.cil.ll/912.smt2	121.730967486	0.067090607
systemc/toy_true.cil.ll/949.smt2	122.967322417	0.056045272

3 Boolector

This is the evaluation on the version of Boolector included in the paper Counterexample-Guided Model Synthesis by M. Preiner, A. Niemetz, and A. Biere, published in TACAS 2017.

3.1 SMT-LIB

3.1.1 Load the results

First, lets get the data and merge them.

simplTimes <- read.csv("simpltimes_smtlib.csv", header=TRUE, stringsAsFactors=FALSE)
smtlib.boolector <- read.csv("boolector_smtlib.csv", header=TRUE, stringsAsFactors=FALSE)
smtlib.boolector_u <- read.csv("boolector_smtlib_unconstrained.csv", header=TRUE, stringsAsFactors=FALSE)

smtlib <- Reduce(function(x, y) merge(x, y, all=TRUE, by="filename"), list(smtlib.boolector, smtlib.boolector_u, simplTimes))
colnames(smtlib) = c('filename', 'result', 'cputime', 'walltime', 'memusage', 'result.u', 'cputime.u', 'walltime.u', 'memusage.u', 'simpltime')

smtlib$cputime[smtlib$result != "sat" & smtlib$result != "unsat"] <- 900
smtlib$walltime[smtlib$result != "sat" & smtlib$result != "unsat"] <- 900
smtlib$cputime.u[smtlib$result.u != "sat" & smtlib$result.u != "unsat"] <- 900
smtlib$walltime.u[smtlib$result.u != "sat" & smtlib$result.u != "unsat"] <- 900

Now, compare number of results of each type for each configuration.

smtlib_standard <- count(smtlib.boolector, "result")
colnames(smtlib_standard) <- c('result', 'standard')

smtlib_unconstrained <- count(smtlib.boolector_u, "result")
colnames(smtlib_unconstrained) <- c('result', 'unconstrained')

Reduce(function(...) merge(..., all=TRUE),
         list(smtlib_standard, smtlib_unconstrained))

result	standard	unconstrained
sat	78	86
timeout	18	10
unsat	95	95

3.1.2 Result counts

This table shows numbers of benchmarks grouped by the result in both of the configurations.

count(smtlib, c('result', 'result.u'))

result	result.u	freq
sat	sat	77
sat	timeout	1
timeout	sat	9
timeout	timeout	9
unsat	unsat	95

3.1.3 Total time/memory

Now, lets see the total CPU time, wall time, memory used and simplification times for both of the configurations.

numcolwise(sum)(smtlib[which((smtlib$result == "sat" & smtlib$result.u == "sat") | (smtlib$result == "unsat" & smtlib$result.u == "unsat")),])

cputime	walltime	memusage	cputime.u	walltime.u	memusage.u	simpltime
1513.451343355	774.232921887189	nil	1257.163370482	647.90848524496	nil	15.8209264478646

3.1.4 Scatter plots

Linear scale

ggplot(smtlib, aes(cputime, cputime.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained", xlim=c(0.001,900), ylim=c(0.001,900)) +
  geom_point() +
  geom_abline(intercept=0) +
  theme(legend.title=element_blank())

Log scale

ggplot(smtlib, aes(cputime, cputime.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained", xlim=c(0.001,900), ylim=c(0.001,900)) +
  geom_point() +
  geom_abline(intercept=0) +
  scale_x_log10(limits = c(0.001, 900), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(limits = c(0.001, 900), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_colour_brewer(palette = "Set1") +
  theme(legend.title=element_blank())

Log scale + simplification time

ggplot(smtlib, aes(cputime, cputime.u + simpltime, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained", xlim=c(0.001,900), ylim=c(0.001,900)) +
  geom_point() +
  geom_abline(intercept=0) +
  scale_x_log10(limits = c(0.001, 901), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(limits = c(0.001, 901), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_colour_brewer(palette = "Set1") +
  theme(legend.title=element_blank())

Memory

ggplot(smtlib, aes(memusage, memusage.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained") +
  geom_point() +
  geom_abline(intercept=0) +
  scale_x_log10(limits = c(1000000,8000000000), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(limits = c(1000000,8000000000), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_colour_brewer(palette = "Set1") +
  theme(legend.title=element_blank())

3.1.5 Quantile plot

smtlib.ordered = sort(smtlib$cputime[smtlib$result == "sat" | smtlib$result == "unsat"]);
smtlib.ordered.u = sort(smtlib$cputime.u[smtlib$result.u == "sat" | smtlib$result.u == "unsat"]);
smtlib.ordered.us = sort((smtlib$cputime.u + smtlib$simpltime)[smtlib$result.u == "sat" | smtlib$result.u == "unsat"]);

plot(c(0, 190), c(0.001, 900), log='y', xlab=NA, ylab=NA, axes=FALSE, frame.plot=TRUE, type='n')

axis(1, at=seq(0,200,50), tck = -.01, label=NA)
axis(2, at=c(0.001,0.1,1,10,100), tck = -.01, label=NA)
axis(1, at=seq(0,200,50), lwd = 0, line = -.8)
axis(2, at=c(0.001,0.01,0.1,1,10,100), labels=c(0.001,0.01,0.1,1,10,100), lwd = 0, line = -.4, las = 1)

lines(1:length(smtlib.ordered), smtlib.ordered, type='s', col='blue')
lines(1:length(smtlib.ordered.u), smtlib.ordered.u, type='s', col='darkgreen')
lines(1:length(smtlib.ordered.us), smtlib.ordered.us, type='s', col='red')

mtext(side = 1, "Formulas from SMT-LIB solved by Boolector", line = 1.2)
mtext(side = 2, "CPU time (s)", line = 2)

legend("topleft",
  lty=c(1,1,1),
  lwd=c(2.5,2.5,2.5),
  col=c("blue", "darkgreen", "red"),
  legend=c("standard", "unconstrained", "unconstrained+simplification time"))

3.1.6 Degraded performance

These are the results where the simplifications increase the solving time by more than 0.5 s.

smtlib[smtlib$cputime + 0.5 < smtlib$cputime.u, c('filename', 'cputime', 'cputime.u')]

filename	cputime	cputime.u
fixpoint/893191/sdlx-fixpoint-7.smt2	20.426631289	21.454481753
ranking/893047/audio_ac97_wavepcistream3.cpp.smt2	3.660193406	17.371056353
ranking/893053/1394diag_ioctl.c.smt2	54.538479993	900
ranking/893055/filesys_smbmrx_cvsndrcv.c.smt2	3.629257681	6.323294118

3.1.7 Improved performance

These are the results where the simplifications decrease the solving time by more than 0.5 s.

smtlib[smtlib$cputime.u + 0.5 < smtlib$cputime, c('filename', 'cputime', 'cputime.u')]

filename	cputime	cputime.u
fixpoint/893082/small-equiv-fixpoint-1.smt2	3.158637551	2.566219448
fixpoint/893097/small-equiv-fixpoint-6.smt2	43.482762424	7.611366943
fixpoint/893103/sdlx-fixpoint-9.smt2	29.953138946	26.153546748
fixpoint/893109/small-equiv-fixpoint-10.smt2	900	15.598443455
fixpoint/893121/small-equiv-fixpoint-9.smt2	900	8.150674285
fixpoint/893125/small-equiv-fixpoint-5.smt2	900	3.048531359
fixpoint/893140/small-equiv-fixpoint-8.smt2	900	7.801856624
fixpoint/893157/small-equiv-fixpoint-3.smt2	900	5.619455545
fixpoint/893175/small-equiv-fixpoint-2.smt2	900	2.813176642
fixpoint/893176/small-equiv-fixpoint-4.smt2	900	5.596781588
fixpoint/893180/sdlx-fixpoint-8.smt2	26.343085107	24.769077185
fixpoint/893184/sdlx-fixpoint-10.smt2	29.167810333	26.773535433
fixpoint/893193/small-equiv-fixpoint-7.smt2	35.457169677	24.059085452
ranking/893013/audio_ddksynth_csynth2.cpp.smt2	9.034440171	6.410712739
ranking/893022/filesys_cdfs_namesup_noarray.c.smt2	347.516493686	168.137963656
ranking/893037/kmdf_usbsamp_sys_queue.c.smt2	107.3733833	76.618730773
ranking/893049/filesys_filter_namelookup.c.smt2	29.321893022	27.06499438
ranking/893056/network_ndis_e100bex_5x_kd_mp_dbg.c.smt2	900	18.705617953
ranking/893062/AVStream_hwsim.cpp.smt2	900	26.527006169

3.2 SymDIVINE

3.2.1 Load the results

First, lets get the data and merge them.

simplTimes <- read.csv("simpltimes_symdivine.csv", header=TRUE, stringsAsFactors=FALSE)
symdivine.boolector <- read.csv("boolector_symdivine.csv", header=TRUE, stringsAsFactors=FALSE)
symdivine.boolector_u <- read.csv("boolector_symdivine_unconstrained.csv", header=TRUE, stringsAsFactors=FALSE)

symdivine <- Reduce(function(x, y) merge(x, y, all=TRUE, by="filename"), list(symdivine.boolector, symdivine.boolector_u, simplTimes))
colnames(symdivine) = c('filename', 'result', 'cputime', 'walltime', 'memusage', 'result.u', 'cputime.u', 'walltime.u', 'memusage.u', 'simpltime')

symdivine$cputime[symdivine$result != "sat" & symdivine$result != "unsat"] <- 900
symdivine$walltime[symdivine$result != "sat" & symdivine$result != "unsat"] <- 900
symdivine$cputime.u[symdivine$result.u != "sat" & symdivine$result.u != "unsat"] <- 900
symdivine$walltime.u[symdivine$result.u != "sat" & symdivine$result.u != "unsat"] <- 900

Now, compare number of results of each type for each configuration.

symdivine_standard <- count(symdivine.boolector, "result")
colnames(symdivine_standard) <- c('result', 'standard')

symdivine_unconstrained <- count(symdivine.boolector_u, "result")
colnames(symdivine_unconstrained) <- c('result', 'unconstrained')

Reduce(function(...) merge(..., all=TRUE),
         list(symdivine_standard, symdivine_unconstrained)) #, symdivine_localunconstrained))

result	standard	unconstrained
ERROR (1)	8	8
sat	1137	1137
timeout	1020	706
unsat	3296	3610

3.2.2 Result counts

This table shows numbers of benchmarks grouped by the result in both of the configurations.

count(symdivine, c('result', 'result.u'))

result	result.u	freq
ERROR (1)	ERROR (1)	8
sat	sat	1137
timeout	timeout	706
timeout	unsat	314
unsat	unsat	3296

3.2.3 Total time/memory

Now, lets see the total CPU time, wall time, memory used and simplification times for both of the configurations.

numcolwise(sum)(symdivine[which((symdivine$result == "sat" & symdivine$result.u == "sat") | (symdivine$result == "unsat" & symdivine$result.u == "unsat")),])

cputime	walltime	memusage	cputime.u	walltime.u	memusage.u	simpltime
20269.869823427	10335.9321458079	nil	1173.964673628	791.669419493526	nil	111.449319924461

3.2.4 Scatter plots

Linear scale

ggplot(symdivine, aes(cputime, cputime.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained", xlim=c(0,900), ylim=c(0,900)) +
  geom_point() +
  geom_abline(intercept=0) +
  scale_colour_brewer(palette = "Set1") +
  theme(legend.title=element_blank())

Log scale

ggplot(symdivine, aes(cputime, cputime.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained") +
  geom_point() +
  geom_abline(intercept=0) +
  scale_x_log10(limits = c(0.001, 900), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(limits = c(0.001, 900), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_colour_brewer(palette = "Set1") +
  theme(legend.title=element_blank())

Log scale + simplification time

ggplot(symdivine, aes(cputime, cputime.u+simpltime, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained") +
  geom_point() +
  geom_abline(intercept=0) +
  scale_x_log10(name="Boolector", limits = c(0.001, 901), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(name="Boolector + simplifications", limits = c(0.001, 901), breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  theme(legend.title=element_blank()) +
  scale_colour_brewer(palette = "Set1") +
  theme(legend.position="none")

3.2.5 Memory

ggplot(symdivine, aes(memusage, memusage.u, colour=factor(result.u, c("timeout", "sat", "unsat", "out of memory"))), xlab = "Standard", ylab = "Unconstrained", log="xy", xlim=c(1000000,8000000000), ylim=c(1000000,8000000000)) +
  geom_point() +
  geom_abline(intercept=0) +
  scale_x_log10(breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_y_log10(breaks = trans_breaks("log10", function(x) 10^x), labels = trans_format("log10", math_format(10^.x))) +
  scale_colour_brewer(palette = "Set1") +
  theme(legend.title=element_blank())

3.2.6 Quantile plot

symdivine.ordered = sort(symdivine$cputime[symdivine$result == "sat" | symdivine$result == "unsat"]);
symdivine.ordered.u = sort(symdivine$cputime.u[symdivine$result.u == "sat" | symdivine$result.u == "unsat"]);
symdivine.ordered.us = sort((symdivine$cputime.u + symdivine$simpltime)[symdivine$result.u == "sat" | symdivine$result.u == "unsat"]);

plot(c(0, 5500), c(0.001, 900), log='y', xlab=NA, ylab=NA, axes=FALSE, frame.plot=TRUE, type='n')

axis(1, at=seq(0,5500,500), tck = -.01, label=NA)
axis(2, at=c(0.001,0.1,1,10,100), tck = -.01, label=NA)
axis(1, at=seq(0,5500,500), lwd = 0, line = -.8)
axis(2, at=c(0.001,0.01,0.1,1,10,100), labels=c(0.001,0.01,0.1,1,10,100), lwd = 0, line = -.4, las = 1)

lines(1:length(symdivine.ordered), symdivine.ordered, type='s', col='blue')
lines(1:length(symdivine.ordered.u), symdivine.ordered.u, type='s', col='darkgreen')
lines(1:length(symdivine.ordered.us), symdivine.ordered.us, type='s', col='red')

mtext(side = 1, "Formulas from SymDIVINE solved by Boolector", line = 1.2)
mtext(side = 2, "CPU time (s)", line = 2)

legend("topleft",
  lty=c(1,1,1),
  lwd=c(2.5,2.5,2.5),
  col=c("blue", "darkgreen", "red"),
  legend=c("standard", "unconstrained", "unconstrained+simplification time"))

3.2.7 Degraded performance

These are the results where the simplifications increase the solving time by more than 0.5 s.

symdivine[symdivine$cputime + 0.5 < symdivine$cputime.u, c('filename', 'cputime', 'cputime.u')]

filename

cputime

cputime.u

3.2.8 Improved performance

These are the results where the simplifications decrease the solving time by more than 0.5 s.

symdivine[symdivine$cputime.u + 0.5 < symdivine$cputime, c('filename', 'cputime', 'cputime.u')]

filename	cputime	cputime.u
bitvector/s3_clnt_1_false.BV.c.cil.ll/1009.smt2	1.101535006	0.029756243
bitvector/s3_clnt_1_false.BV.c.cil.ll/1020.smt2	1.533732378	0.04323951
bitvector/s3_clnt_1_false.BV.c.cil.ll/441.smt2	14.033545068	0.038723243
bitvector/s3_clnt_1_false.BV.c.cil.ll/596.smt2	2.037858386	0.033542885
bitvector/s3_clnt_1_false.BV.c.cil.ll/603.smt2	7.192881074	0.039114449
bitvector/s3_clnt_1_false.BV.c.cil.ll/693.smt2	0.86799725	0.040568311
bitvector/s3_clnt_1_false.BV.c.cil.ll/705.smt2	1.185113123	0.04604261
bitvector/s3_clnt_1_false.BV.c.cil.ll/733.smt2	1.62198218	0.036343002
bitvector/s3_clnt_1_false.BV.c.cil.ll/861.smt2	3.899225885	0.039290674
bitvector/s3_clnt_1_false.BV.c.cil.ll/881.smt2	1.390047376	0.031913692
bitvector/s3_clnt_1_false.BV.c.cil.ll/893.smt2	2.744968297	0.041051571
bitvector/s3_clnt_1_false.BV.c.cil.ll/954.smt2	1.892382264	0.032357071
bitvector/s3_clnt_1_false.BV.c.cil.ll/998.smt2	3.342600876	0.045743184
bitvector/s3_clnt_1_true.BV.c.cil.ll/10416.smt2	2.267539354	0.029939224
bitvector/s3_clnt_1_true.BV.c.cil.ll/10486.smt2	2.569220939	0.033062526
bitvector/s3_clnt_1_true.BV.c.cil.ll/10859.smt2	14.008112075	0.036349229
bitvector/s3_clnt_1_true.BV.c.cil.ll/12160.smt2	6.744787173	0.041052619
bitvector/s3_clnt_1_true.BV.c.cil.ll/12472.smt2	1.636041206	0.040807891
bitvector/s3_clnt_1_true.BV.c.cil.ll/12914.smt2	4.966299069	0.046295148
bitvector/s3_clnt_1_true.BV.c.cil.ll/14584.smt2	8.462253705	0.033201742
bitvector/s3_clnt_1_true.BV.c.cil.ll/15061.smt2	5.135824667	0.040171761
bitvector/s3_clnt_1_true.BV.c.cil.ll/15165.smt2	3.658687409	0.036151496
bitvector/s3_clnt_1_true.BV.c.cil.ll/16157.smt2	1.295835976	0.033685062
bitvector/s3_clnt_1_true.BV.c.cil.ll/16690.smt2	3.129342736	0.035242282
bitvector/s3_clnt_1_true.BV.c.cil.ll/17312.smt2	1.252595936	0.041163577
bitvector/s3_clnt_1_true.BV.c.cil.ll/17397.smt2	2.985614541	0.042938228
bitvector/s3_clnt_1_true.BV.c.cil.ll/17674.smt2	2.408431018	0.036749131
bitvector/s3_clnt_1_true.BV.c.cil.ll/19112.smt2	1.318336483	0.028925718
bitvector/s3_clnt_1_true.BV.c.cil.ll/22503.smt2	8.66413747	0.037535397
bitvector/s3_clnt_1_true.BV.c.cil.ll/22557.smt2	2.723230178	0.033535924
bitvector/s3_clnt_1_true.BV.c.cil.ll/23350.smt2	2.042016825	0.037585815
bitvector/s3_clnt_1_true.BV.c.cil.ll/23378.smt2	0.820693464	0.032896918
bitvector/s3_clnt_1_true.BV.c.cil.ll/5994.smt2	0.624829579	0.028192014
bitvector/s3_clnt_1_true.BV.c.cil.ll/6496.smt2	1.363696855	0.032558108
bitvector/s3_clnt_1_true.BV.c.cil.ll/6647.smt2	0.977983534	0.033197352
bitvector/s3_clnt_1_true.BV.c.cil.ll/6863.smt2	4.484692769	0.034213568
bitvector/s3_clnt_1_true.BV.c.cil.ll/7954.smt2	2.615523395	0.033019401
bitvector/s3_clnt_1_true.BV.c.cil.ll/8211.smt2	2.338184778	0.038287167
bitvector/s3_clnt_2_true.BV.c.cil.ll/10416.smt2	2.479635504	0.039102044
bitvector/s3_clnt_2_true.BV.c.cil.ll/11133.smt2	1.911504276	0.038643146
bitvector/s3_clnt_2_true.BV.c.cil.ll/12861.smt2	2.230728305	0.03999645
bitvector/s3_clnt_2_true.BV.c.cil.ll/12886.smt2	2.335781035	0.041658748
bitvector/s3_clnt_2_true.BV.c.cil.ll/8053.smt2	1.930669974	0.040375168
bitvector/s3_clnt_2_true.BV.c.cil.ll/9907.smt2	9.373576997	0.041109137
bitvector/s3_clnt_3_true.BV.c.cil.ll/10767.smt2	2.011658554	0.039680228
bitvector/s3_clnt_3_true.BV.c.cil.ll/13428.smt2	2.840136787	0.040155699
bitvector/s3_clnt_3_true.BV.c.cil.ll/14003.smt2	2.32694928	0.040850951
bitvector/s3_clnt_3_true.BV.c.cil.ll/3891.smt2	1.607464116	0.03541282
bitvector/s3_clnt_3_true.BV.c.cil.ll/6295.smt2	2.186463909	0.033005051
bitvector/s3_clnt_3_true.BV.c.cil.ll/6468.smt2	1.508963849	0.039535574
bitvector/s3_clnt_3_true.BV.c.cil.ll/8395.smt2	8.500494453	0.042044207
bitvector/s3_srvr_2_alt_true.BV.c.cil.ll/185.smt2	900	0.086668383
bitvector/s3_srvr_2_alt_true.BV.c.cil.ll/24.smt2	900	0.081390199
bitvector/s3_srvr_2_alt_true.BV.c.cil.ll/30.smt2	900	0.085993105
bitvector/s3_srvr_2_alt_true.BV.c.cil.ll/70.smt2	0.742029066	0.082067586
bitvector/s3_srvr_2_true.BV.c.cil.ll/1.smt2	900	0.068245117
bitvector/s3_srvr_2_true.BV.c.cil.ll/3.smt2	900	0.113470022
bitvector/s3_srvr_2_true.BV.c.cil.ll/54.smt2	900	0.056630051
bitvector/s3_srvr_2_true.BV.c.cil.ll/92.smt2	900	0.06258211
eca/Problem01_10_true.ll/1625.smt2	900	0.231365639
eca/Problem01_20_false.ll/1161.smt2	900	0.22444567
eca/Problem01_20_false.ll/699.smt2	900	0.126863493
eca/Problem01_30_true.ll/1309.smt2	900	0.24824142
eca/Problem01_30_true.ll/39.smt2	900	0.131412325
eca/Problem03_00_true.ll/507.smt2	900	0.121829257
eca/Problem03_10_true.ll/2874.smt2	900	0.142674824
eca/Problem03_20_true.ll/1667.smt2	900	0.087471177
eca/Problem03_20_true.ll/26.smt2	900	0.087441255
eca/Problem03_20_true.ll/3762.smt2	900	0.204176995
eca/Problem03_20_true.ll/5203.smt2	900	0.139558579
eca/Problem03_30_true.ll/1683.smt2	900	0.088733355
eca/Problem03_30_true.ll/2126.smt2	900	0.182342235
eca/Problem03_30_true.ll/4894.smt2	900	0.20533795
eca/Problem03_30_true.ll/687.smt2	900	0.122766918
eca/Problem03_40_true.ll/1828.smt2	900	0.087455026
eca/Problem03_40_true.ll/1840.smt2	900	0.147100366
eca/Problem03_40_true.ll/355.smt2	900	0.122470437
eca/Problem03_40_true.ll/587.smt2	900	0.124485964
eca/Problem03_50_false.ll/1668.smt2	900	0.086552569
eca/Problem03_50_false.ll/1676.smt2	900	0.09030943
eca/Problem03_50_false.ll/2306.smt2	900	0.178960365
eca/Problem03_50_false.ll/3034.smt2	900	0.144299146
eca/Problem03_50_false.ll/4.smt2	900	0.087308589
eca/Problem03_50_false.ll/5110.smt2	900	0.205917161
eca/Problem03_50_false.ll/5288.smt2	900	0.201572924
eca/Problem03_50_false.ll/647.smt2	900	0.12307512
eca/Problem04_00_true.ll/1415.smt2	900	0.195553214
eca/Problem04_00_true.ll/2197.smt2	900	0.190644568
eca/Problem04_00_true.ll/2497.smt2	900	0.244077926
eca/Problem04_00_true.ll/2537.smt2	900	0.247442001
eca/Problem04_00_true.ll/2557.smt2	900	0.243982835
eca/Problem04_00_true.ll/2707.smt2	900	0.237608504
eca/Problem04_10_true.ll/1322.smt2	900	0.1967128
eca/Problem04_10_true.ll/2055.smt2	900	0.125329495
eca/Problem04_10_true.ll/2333.smt2	900	0.19395144
eca/Problem04_10_true.ll/2755.smt2	900	0.199130885
eca/Problem04_10_true.ll/2775.smt2	900	0.192965413
eca/Problem04_20_true.ll/101.smt2	900	0.109028746
eca/Problem04_20_true.ll/2341.smt2	900	0.188419913
eca/Problem04_20_true.ll/2362.smt2	900	0.199451735
eca/Problem04_20_true.ll/2565.smt2	900	0.190195468
eca/Problem04_20_true.ll/2731.smt2	900	0.200606946
eca/Problem04_30_true.ll/2261.smt2	900	0.19511654
eca/Problem04_30_true.ll/2480.smt2	900	0.195418326
eca/Problem04_30_true.ll/2526.smt2	900	0.198164382
eca/Problem04_30_true.ll/2590.smt2	900	0.197734469
eca/Problem04_40_false.ll/1229.smt2	900	0.19691987
eca/Problem04_40_false.ll/1253.smt2	900	0.195037997
eca/Problem04_40_false.ll/2133.smt2	900	0.197260632
eca/Problem04_40_false.ll/2557.smt2	900	0.240336084
eca/Problem04_50_true.ll/1265.smt2	900	0.195534586
eca/Problem04_50_true.ll/1295.smt2	900	0.194693897
eca/Problem04_50_true.ll/1412.smt2	900	0.196710197
eca/Problem04_50_true.ll/2130.smt2	900	0.204945041
eca/Problem04_50_true.ll/2221.smt2	900	0.194346479
eca/Problem04_50_true.ll/2710.smt2	900	0.190712863
eca/Problem04_50_true.ll/2722.smt2	900	0.234197351
eca/Problem05_00_false.ll/74.smt2	900	0.122359487
eca/Problem05_00_false.ll/93.smt2	900	0.117352834
eca/Problem05_10_true.ll/128.smt2	900	0.12186587
eca/Problem05_10_true.ll/45.smt2	900	0.123621914
eca/Problem05_10_true.ll/88.smt2	900	0.138030255
eca/Problem05_20_true.ll/153.smt2	900	0.122533284
eca/Problem05_20_true.ll/40.smt2	900	0.117945866
eca/Problem05_20_true.ll/80.smt2	900	0.114683738
eca/Problem05_20_true.ll/85.smt2	900	0.123478536
eca/Problem05_30_false.ll/137.smt2	900	0.122523722
eca/Problem05_30_false.ll/143.smt2	900	0.123406844
eca/Problem05_30_false.ll/160.smt2	900	0.116028523
eca/Problem05_40_false.ll/48.smt2	900	0.122410545
eca/Problem05_40_false.ll/67.smt2	900	0.121689095
eca/Problem05_40_false.ll/80.smt2	900	0.121185134
eca/Problem05_50_true.ll/158.smt2	900	0.122225704
eca/Problem05_50_true.ll/46.smt2	900	0.123361152
eca/Problem06_00_false.ll/743.smt2	900	0.112890721
eca/Problem06_50_true.ll/1165.smt2	900	0.167941602
eca/Problem11_00_false.ll/1082.smt2	900	0.211381615
eca/Problem11_00_false.ll/6240.smt2	900	0.216751388
eca/Problem11_10_false.ll/2439.smt2	900	0.125218392
eca/Problem11_10_false.ll/3805.smt2	900	0.227380596
eca/Problem11_50_false.ll/6542.smt2	900	0.25343074
eca/Problem12_00_false.ll/1509.smt2	900	0.103432192
eca/Problem12_00_false.ll/2574.smt2	900	0.203630331
eca/Problem12_10_false.ll/1584.smt2	900	0.103068135
eca/Problem12_10_false.ll/1635.smt2	900	0.09807296
eca/Problem12_10_false.ll/2767.smt2	900	0.098697713
eca/Problem12_10_false.ll/2807.smt2	900	0.209957237
eca/Problem12_10_false.ll/829.smt2	900	0.189638182
eca/Problem12_20_false.ll/1542.smt2	900	0.099341116
eca/Problem12_20_false.ll/2675.smt2	900	0.096948318
eca/Problem12_20_false.ll/2742.smt2	900	0.207674846
eca/Problem12_30_false.ll/1606.smt2	900	0.104733494
eca/Problem12_30_false.ll/2553.smt2	900	0.205520361
eca/Problem12_30_false.ll/3.smt2	18.54072461	0.103560584
eca/Problem12_30_false.ll/841.smt2	900	0.182903924
eca/Problem12_30_false.ll/929.smt2	900	0.18260293
eca/Problem12_40_false.ll/1470.smt2	900	0.090381169
eca/Problem12_40_false.ll/1624.smt2	900	0.09579883
eca/Problem12_40_false.ll/2534.smt2	900	0.097857666
eca/Problem12_40_false.ll/2617.smt2	900	0.206968653
eca/Problem12_40_false.ll/797.smt2	900	0.187353837
eca/Problem12_50_false.ll/1604.smt2	900	0.10461366
eca/Problem12_50_false.ll/1763.smt2	900	0.098685118
eca/Problem12_50_false.ll/1773.smt2	900	0.1808803
eca/Problem12_50_false.ll/2556.smt2	900	0.212323402
eca/Problem12_50_false.ll/919.smt2	900	0.185661794
eca/Problem13_00_false.ll/105.smt2	900	0.146019069
eca/Problem13_10_false.ll/143.smt2	900	0.13951255
eca/Problem13_30_false.ll/82.smt2	900	0.138696289
eca/Problem13_30_false.ll/88.smt2	900	0.138512558
eca/Problem13_40_false.ll/172.smt2	900	0.138193356
eca/Problem14_00_true.ll/599.smt2	900	0.148438606
eca/Problem14_10_false.ll/2761.smt2	900	0.257986737
eca/Problem14_20_true.ll/2309.smt2	900	0.338960952
eca/Problem15_00_false.ll/3471.smt2	900	0.401733178
eca/Problem15_00_false.ll/4113.smt2	900	0.091772139
eca/Problem15_20_false.ll/691.smt2	900	0.203081319
eca/Problem15_40_false.ll/4099.smt2	900	0.099874797
eca/Problem16_00_false.ll/534.smt2	900	0.130825456
eca/Problem16_00_false.ll/965.smt2	900	0.150029303
eca/Problem16_08_false.ll/1066.smt2	900	0.14666061
eca/Problem16_08_false.ll/715.smt2	900	0.143402702
eca/Problem16_08_false.ll/720.smt2	900	0.162919488
eca/Problem16_08_false.ll/868.smt2	900	0.256233855
eca/Problem16_08_false.ll/882.smt2	900	0.16381987
eca/Problem16_20_false.ll/2339.smt2	900	0.233695308
eca/Problem16_20_false.ll/762.smt2	900	0.163773186
eca/Problem16_20_false.ll/930.smt2	900	0.246796257
eca/Problem16_40_false.ll/1072.smt2	900	0.247136891
eca/Problem16_40_false.ll/1107.smt2	900	0.16011811
eca/Problem16_40_false.ll/3851.smt2	900	0.106535944
eca/Problem16_40_false.ll/721.smt2	900	0.137382468
eca/Problem16_40_false.ll/724.smt2	900	0.152498664
eca/Problem16_40_false.ll/906.smt2	900	0.153521819
eca/Problem16_50_true.ll/1824.smt2	900	0.103494759
eca/Problem16_60_false.ll/4428.smt2	900	0.274412128
eca/Problem17_00_false.ll/1176.smt2	900	0.147444428
eca/Problem17_00_false.ll/541.smt2	900	0.18686916
eca/Problem17_10_false.ll/1924.smt2	900	0.0962618
eca/Problem17_10_false.ll/52.smt2	900	0.100672974
eca/Problem17_20_false.ll/1067.smt2	900	0.096772321
eca/Problem17_20_false.ll/1689.smt2	900	0.123474513
eca/Problem17_30_false.ll/1138.smt2	900	0.143727699
eca/Problem17_30_false.ll/1557.smt2	900	0.14757949
eca/Problem17_30_false.ll/1586.smt2	900	0.142814657
eca/Problem17_30_false.ll/3894.smt2	900	0.150808118
eca/Problem17_40_false.ll/92.smt2	900	0.130937532
eca/Problem17_40_false.ll/987.smt2	900	0.136522668
eca/Problem17_50_false.ll/1524.smt2	900	0.194826376
eca/Problem17_50_false.ll/3724.smt2	900	0.206789276
eca/Problem17_60_false.ll/1097.smt2	900	0.139905347
eca/Problem17_60_false.ll/1177.smt2	900	0.142056017
eca/Problem17_60_false.ll/218.smt2	900	0.152596877
eca/Problem18_10_false.ll/1289.smt2	900	0.090041317
eca/Problem18_10_false.ll/657.smt2	900	0.18366212
eca/Problem18_20_false.ll/2232.smt2	900	0.237426209
eca/Problem18_30_false.ll/412.smt2	900	0.109871224
eca/Problem18_30_false.ll/693.smt2	900	0.199661992
eca/Problem18_50_false.ll/2149.smt2	900	0.237851211
eca/Problem19_00_false.ll/1274.smt2	900	0.158205778
eca/Problem19_00_false.ll/307.smt2	900	0.14941347
eca/Problem19_00_false.ll/313.smt2	900	0.14931004
eca/Problem19_00_false.ll/318.smt2	900	0.135881831
eca/Problem19_00_false.ll/390.smt2	900	0.137243911
eca/Problem19_10_false.ll/1296.smt2	900	0.153915098
eca/Problem19_10_false.ll/1323.smt2	900	0.144795229
eca/Problem19_10_false.ll/1358.smt2	900	0.144243589
eca/Problem19_10_false.ll/1386.smt2	900	0.160532886
eca/Problem19_10_false.ll/291.smt2	900	0.133312684
eca/Problem19_10_false.ll/326.smt2	900	0.136885246
eca/Problem19_10_false.ll/358.smt2	900	0.140092233
eca/Problem19_10_false.ll/550.smt2	900	0.129944512
eca/Problem19_20_false.ll/1254.smt2	900	0.161408644
eca/Problem19_20_false.ll/1350.smt2	900	0.155545006
eca/Problem19_20_false.ll/338.smt2	900	0.15077637
eca/Problem19_30_false.ll/1277.smt2	900	0.142071203
eca/Problem19_30_false.ll/1293.smt2	900	0.158606592
eca/Problem19_30_false.ll/1341.smt2	900	0.15999776
eca/Problem19_30_false.ll/303.smt2	900	0.148518571
eca/Problem19_30_false.ll/344.smt2	900	0.139063686
eca/Problem19_30_false.ll/387.smt2	900	0.138609465
eca/Problem19_38_false.ll/1241.smt2	900	0.13445129
eca/Problem19_38_false.ll/1289.smt2	900	0.138577859
eca/Problem19_38_false.ll/315.smt2	900	0.140301008
eca/Problem19_38_false.ll/397.smt2	900	0.154571511
eca/Problem19_50_false.ll/1198.smt2	900	0.13935083
eca/Problem19_50_false.ll/1356.smt2	900	0.151090914
eca/Problem19_50_false.ll/1421.smt2	900	0.137898067
eca/Problem19_50_false.ll/326.smt2	900	0.146801839
eca/Problem19_50_false.ll/376.smt2	900	0.146860499
eca/Problem19_50_false.ll/403.smt2	900	0.138496168
locks/test_locks_10_true.ll/10455.smt2	0.539986608	0.023881953
locks/test_locks_10_true.ll/11656.smt2	0.674168736	0.026113771
locks/test_locks_10_true.ll/12219.smt2	1.644524771	0.023403315
locks/test_locks_10_true.ll/3306.smt2	0.680234238	0.033530421
locks/test_locks_10_true.ll/4453.smt2	0.857859606	0.026843883
locks/test_locks_10_true.ll/5928.smt2	0.60748895	0.040238427
locks/test_locks_10_true.ll/5993.smt2	1.153314796	0.031695078
locks/test_locks_10_true.ll/6417.smt2	1.005661635	0.029996607
locks/test_locks_10_true.ll/7331.smt2	0.894201375	0.027988091
locks/test_locks_10_true.ll/7536.smt2	0.596611274	0.025747544
locks/test_locks_10_true.ll/7836.smt2	1.039677007	0.028810726
locks/test_locks_10_true.ll/8574.smt2	0.833461893	0.026863
locks/test_locks_10_true.ll/8762.smt2	1.349388431	0.03179618
locks/test_locks_10_true.ll/9037.smt2	1.503842036	0.027398958
locks/test_locks_10_true.ll/9287.smt2	1.301777574	0.030133131
locks/test_locks_11_true.ll/11853.smt2	1.055575334	0.032273663
locks/test_locks_11_true.ll/12600.smt2	0.77989294	0.026548375
locks/test_locks_11_true.ll/13818.smt2	1.635554559	0.025700064
locks/test_locks_11_true.ll/14872.smt2	2.180908426	0.026192065
locks/test_locks_11_true.ll/2622.smt2	0.636564878	0.02581576
locks/test_locks_11_true.ll/5971.smt2	0.956793739	0.028630081
locks/test_locks_11_true.ll/6045.smt2	0.678354243	0.028515848
locks/test_locks_11_true.ll/6204.smt2	1.074672198	0.032284144
locks/test_locks_11_true.ll/6397.smt2	0.848969584	0.028046477
locks/test_locks_11_true.ll/6659.smt2	1.160862467	0.0275493
locks/test_locks_11_true.ll/8248.smt2	1.361432286	0.026156757
locks/test_locks_11_true.ll/9281.smt2	1.231924917	0.028020672
locks/test_locks_11_true.ll/9313.smt2	1.553685126	0.0280009
locks/test_locks_11_true.ll/9366.smt2	0.788152904	0.031314194
locks/test_locks_12_true.ll/10839.smt2	1.387717779	0.029913135
locks/test_locks_12_true.ll/11546.smt2	1.030456771	0.027804665
locks/test_locks_12_true.ll/12158.smt2	1.036094828	0.021380988
locks/test_locks_12_true.ll/13906.smt2	0.867716609	0.031413517
locks/test_locks_12_true.ll/3453.smt2	0.581694774	0.028573079
locks/test_locks_12_true.ll/4502.smt2	0.53296231	0.026420058
locks/test_locks_12_true.ll/4614.smt2	0.638894148	0.023266705
locks/test_locks_12_true.ll/5930.smt2	0.627399822	0.02595208
locks/test_locks_12_true.ll/6768.smt2	1.097478129	0.026548875
locks/test_locks_12_true.ll/7342.smt2	1.022876141	0.025193784
locks/test_locks_12_true.ll/7479.smt2	1.12815784	0.032590641
locks/test_locks_12_true.ll/7866.smt2	1.308477988	0.026496541
locks/test_locks_12_true.ll/7926.smt2	0.751089861	0.029532433
locks/test_locks_12_true.ll/9094.smt2	0.771478398	0.02687855
locks/test_locks_12_true.ll/9229.smt2	0.772347467	0.024030769
locks/test_locks_12_true.ll/9940.smt2	0.983098814	0.026201569
locks/test_locks_13_true.ll/10099.smt2	0.568901797	0.008731884
locks/test_locks_13_true.ll/10340.smt2	0.665051583	0.009353686
locks/test_locks_13_true.ll/10643.smt2	0.951653543	0.022684382
locks/test_locks_13_true.ll/12306.smt2	0.630701482	0.026784978
locks/test_locks_13_true.ll/14039.smt2	0.630445036	0.015697336
locks/test_locks_13_true.ll/14400.smt2	0.81885263	0.026092382
locks/test_locks_13_true.ll/15757.smt2	0.708216169	0.010578849
locks/test_locks_13_true.ll/15975.smt2	0.605475494	0.010036322
locks/test_locks_13_true.ll/16642.smt2	0.877588981	0.026233127
locks/test_locks_13_true.ll/17851.smt2	0.838502804	0.010980493
locks/test_locks_13_true.ll/18068.smt2	0.660289365	0.010401641
locks/test_locks_13_true.ll/18346.smt2	0.7033915	0.01070318
locks/test_locks_14_true.ll/10372.smt2	1.057377522	0.035772483
locks/test_locks_14_true.ll/10717.smt2	1.617060859	0.026621967
locks/test_locks_14_true.ll/10810.smt2	1.100439196	0.027041769
locks/test_locks_14_true.ll/11846.smt2	0.987919691	0.02708006
locks/test_locks_14_true.ll/11977.smt2	0.791321714	0.028247679
locks/test_locks_14_true.ll/12446.smt2	0.811486765	0.02833836
locks/test_locks_14_true.ll/13733.smt2	0.79703763	0.03156232
locks/test_locks_14_true.ll/13786.smt2	1.325596661	0.027984741
locks/test_locks_14_true.ll/15419.smt2	0.65622739	0.026103512
locks/test_locks_14_true.ll/4733.smt2	0.839985778	0.029162114
locks/test_locks_14_true.ll/5555.smt2	1.021493926	0.02498331
locks/test_locks_14_true.ll/5716.smt2	0.62548915	0.035580412
locks/test_locks_14_true.ll/5844.smt2	0.789142016	0.023049209
locks/test_locks_14_true.ll/6403.smt2	0.896879437	0.027251762
locks/test_locks_14_true.ll/6549.smt2	1.17718503	0.027357517
locks/test_locks_14_true.ll/7845.smt2	1.127981773	0.033019054
locks/test_locks_14_true.ll/9107.smt2	0.879349664	0.027571804
locks/test_locks_14_true.ll/9533.smt2	1.057598667	0.023849155
locks/test_locks_14_true.ll/9656.smt2	0.918675177	0.044332756
locks/test_locks_15_true.ll/10125.smt2	1.413075445	0.025507052
locks/test_locks_15_true.ll/11153.smt2	1.570630743	0.026573695
locks/test_locks_15_true.ll/11203.smt2	0.660831232	0.026432837
locks/test_locks_15_true.ll/13343.smt2	1.820563797	0.029655768
locks/test_locks_15_true.ll/14253.smt2	0.982082408	0.023055204
locks/test_locks_15_true.ll/2472.smt2	0.561464966	0.026030177
locks/test_locks_15_true.ll/2551.smt2	0.629983312	0.027369932
locks/test_locks_15_true.ll/2824.smt2	0.528607201	0.026024277
locks/test_locks_15_true.ll/3059.smt2	0.611826978	0.031477551
locks/test_locks_15_true.ll/4153.smt2	0.686139352	0.027548158
locks/test_locks_15_true.ll/5850.smt2	0.846060434	0.031903394
locks/test_locks_15_true.ll/6481.smt2	0.623687382	0.025038524
locks/test_locks_15_true.ll/7222.smt2	0.989096235	0.027621368
locks/test_locks_15_true.ll/8170.smt2	0.683095975	0.027955013
locks/test_locks_15_true.ll/8426.smt2	0.681361093	0.027910617
locks/test_locks_5_true.ll/10086.smt2	1.036478055	0.027619162
locks/test_locks_5_true.ll/10635.smt2	0.828517217	0.02564417
locks/test_locks_5_true.ll/11680.smt2	0.871449501	0.037049581
locks/test_locks_5_true.ll/12173.smt2	1.185924827	0.028718986
locks/test_locks_5_true.ll/12296.smt2	0.874913399	0.046018953
locks/test_locks_5_true.ll/12511.smt2	1.441208942	0.023453921
locks/test_locks_5_true.ll/14257.smt2	1.02562651	0.028383216
locks/test_locks_5_true.ll/15281.smt2	1.011884959	0.028032427
locks/test_locks_5_true.ll/3400.smt2	0.780177146	0.028103191
locks/test_locks_5_true.ll/4626.smt2	0.738496036	0.028880619
locks/test_locks_5_true.ll/5418.smt2	0.742236756	0.03271894
locks/test_locks_5_true.ll/5518.smt2	0.712515621	0.025133415
locks/test_locks_5_true.ll/6898.smt2	1.228468659	0.023990671
locks/test_locks_5_true.ll/7606.smt2	1.177346551	0.02637503
locks/test_locks_5_true.ll/7616.smt2	1.278058702	0.029156485
locks/test_locks_5_true.ll/8289.smt2	0.620211756	0.026505524
locks/test_locks_5_true.ll/9122.smt2	1.009286185	0.024630307
locks/test_locks_5_true.ll/9954.smt2	1.111230233	0.027271374
locks/test_locks_6_true.ll/10096.smt2	1.125106325	0.026693206
locks/test_locks_6_true.ll/10110.smt2	1.250565646	0.02766563
locks/test_locks_6_true.ll/10679.smt2	1.239043703	0.026572393
locks/test_locks_6_true.ll/10775.smt2	0.774017174	0.036566285
locks/test_locks_6_true.ll/11449.smt2	1.557817037	0.026393374
locks/test_locks_6_true.ll/13517.smt2	1.940683935	0.02869863
locks/test_locks_6_true.ll/13748.smt2	0.931297791	0.027447546
locks/test_locks_6_true.ll/13981.smt2	1.610881815	0.02744205
locks/test_locks_6_true.ll/14374.smt2	0.545416647	0.035331952
locks/test_locks_6_true.ll/14598.smt2	1.044139865	0.037659395
locks/test_locks_6_true.ll/3071.smt2	0.680214325	0.02324331
locks/test_locks_6_true.ll/5444.smt2	0.949653971	0.02559622
locks/test_locks_6_true.ll/5982.smt2	1.044991175	0.025498015
locks/test_locks_6_true.ll/7046.smt2	0.536204333	0.028378658
locks/test_locks_6_true.ll/8869.smt2	1.128685177	0.024138087
locks/test_locks_7_true.ll/10564.smt2	1.524729172	0.028336376
locks/test_locks_7_true.ll/11210.smt2	0.707944833	0.028305684
locks/test_locks_7_true.ll/12398.smt2	1.904754388	0.026399909
locks/test_locks_7_true.ll/13959.smt2	1.387177893	0.028792961
locks/test_locks_7_true.ll/13992.smt2	1.751335762	0.026159768
locks/test_locks_7_true.ll/14010.smt2	1.942718896	0.023609562
locks/test_locks_7_true.ll/14076.smt2	0.89042184	0.025692658
locks/test_locks_7_true.ll/14964.smt2	1.314077304	0.023734007
locks/test_locks_7_true.ll/3814.smt2	0.756021706	0.025925662
locks/test_locks_7_true.ll/4795.smt2	0.571170483	0.032184091
locks/test_locks_7_true.ll/6498.smt2	0.753833418	0.029080309
locks/test_locks_7_true.ll/6782.smt2	1.231364032	0.031065666
locks/test_locks_7_true.ll/7996.smt2	1.365277351	0.031594725
locks/test_locks_7_true.ll/8460.smt2	0.974843343	0.029610465
locks/test_locks_7_true.ll/9223.smt2	0.73212235	0.022958953
locks/test_locks_7_true.ll/9526.smt2	1.002555215	0.0299475
locks/test_locks_7_true.ll/9553.smt2	1.242546298	0.027108865
locks/test_locks_8_true.ll/10864.smt2	1.707239449	0.02584442
locks/test_locks_8_true.ll/12801.smt2	1.240695067	0.028214629
locks/test_locks_8_true.ll/12972.smt2	1.296239703	0.028374688
locks/test_locks_8_true.ll/13137.smt2	1.359953608	0.02809347
locks/test_locks_8_true.ll/13493.smt2	1.671737173	0.028003177
locks/test_locks_8_true.ll/14143.smt2	1.670854656	0.027058631
locks/test_locks_8_true.ll/15152.smt2	1.548810691	0.028886631
locks/test_locks_8_true.ll/15351.smt2	1.738215146	0.025214495
locks/test_locks_8_true.ll/2540.smt2	0.551500386	0.027337286
locks/test_locks_8_true.ll/4076.smt2	0.75748975	0.025867025
locks/test_locks_8_true.ll/5036.smt2	0.952228466	0.027458725
locks/test_locks_8_true.ll/5242.smt2	0.969112809	0.024928666
locks/test_locks_8_true.ll/5845.smt2	0.806035907	0.035584062
locks/test_locks_8_true.ll/8438.smt2	0.817476413	0.027811762
locks/test_locks_8_true.ll/8683.smt2	0.665529234	0.027273671
locks/test_locks_8_true.ll/9807.smt2	1.100488651	0.029315304
locks/test_locks_8_true.ll/9810.smt2	1.075410425	0.031274505
locks/test_locks_9_true.ll/10112.smt2	1.289749842	0.026922147
locks/test_locks_9_true.ll/10465.smt2	0.646930061	0.025887883
locks/test_locks_9_true.ll/11097.smt2	1.033318095	0.0257612
locks/test_locks_9_true.ll/11130.smt2	1.425763111	0.022395536
locks/test_locks_9_true.ll/11312.smt2	1.80368051	0.024274461
locks/test_locks_9_true.ll/11730.smt2	1.33500305	0.027447983
locks/test_locks_9_true.ll/11960.smt2	0.646673795	0.023856414
locks/test_locks_9_true.ll/13903.smt2	0.834604944	0.023732494
locks/test_locks_9_true.ll/14259.smt2	1.039229756	0.025557055
locks/test_locks_9_true.ll/15009.smt2	1.90709403	0.023594361
locks/test_locks_9_true.ll/5525.smt2	0.82630783	0.02642166
locks/test_locks_9_true.ll/7476.smt2	1.110731995	0.030466462
locks/test_locks_9_true.ll/7578.smt2	0.944925803	0.035476915
locks/test_locks_9_true.ll/7650.smt2	0.570351443	0.027446955
locks/test_locks_9_true.ll/7914.smt2	0.681703892	0.024037998
locks/test_locks_9_true.ll/7925.smt2	0.747238873	0.024377748
locks/test_locks_9_true.ll/8228.smt2	1.194509448	0.03241652
locks/test_locks_9_true.ll/9272.smt2	1.163591163	0.024409155
ssh-simplified/s3_clnt_1_true.cil.ll/10956.smt2	0.960292952	0.045274383
ssh-simplified/s3_clnt_1_true.cil.ll/13310.smt2	900	0.047347508
ssh-simplified/s3_clnt_1_true.cil.ll/16222.smt2	2.744811602	0.047237932
ssh-simplified/s3_clnt_1_true.cil.ll/5552.smt2	2.3814481	0.042943113
ssh-simplified/s3_clnt_1_true.cil.ll/5916.smt2	1.614212861	0.044021473
ssh-simplified/s3_clnt_1_true.cil.ll/6343.smt2	900	0.044025965
ssh-simplified/s3_clnt_1_true.cil.ll/7857.smt2	1.589264229	0.039963846
ssh-simplified/s3_clnt_1_true.cil.ll/8386.smt2	4.108899408	0.044028363
ssh-simplified/s3_clnt_1_true.cil.ll/9815.smt2	5.443854357	0.046038161
ssh-simplified/s3_clnt_2_true.cil.ll/3641.smt2	2.289889946	0.037545502
ssh-simplified/s3_clnt_2_true.cil.ll/3783.smt2	1.598525935	0.043509892
ssh-simplified/s3_clnt_2_true.cil.ll/6071.smt2	2.458053592	0.042442787
ssh-simplified/s3_clnt_2_true.cil.ll/6215.smt2	3.500193066	0.047415805
ssh-simplified/s3_clnt_2_true.cil.ll/6870.smt2	1.279333855	0.043097884
ssh-simplified/s3_clnt_2_true.cil.ll/8013.smt2	1.558497161	0.043796166
ssh-simplified/s3_clnt_3_true.cil.ll/11020.smt2	1.859349514	0.037492519
ssh-simplified/s3_clnt_3_true.cil.ll/11616.smt2	2.557651345	0.043905063
ssh-simplified/s3_clnt_3_true.cil.ll/12075.smt2	3.208849616	0.04088521
ssh-simplified/s3_clnt_3_true.cil.ll/13855.smt2	5.09781779	0.038836305
ssh-simplified/s3_clnt_3_true.cil.ll/13879.smt2	900	0.041995618
ssh-simplified/s3_clnt_3_true.cil.ll/15992.smt2	1.865552671	0.04001301
ssh-simplified/s3_clnt_3_true.cil.ll/3901.smt2	1.338019148	0.041846429
ssh-simplified/s3_clnt_3_true.cil.ll/4700.smt2	0.904437725	0.043728285
ssh-simplified/s3_clnt_3_true.cil.ll/5219.smt2	900	0.046200503
ssh-simplified/s3_clnt_3_true.cil.ll/7005.smt2	1.785211428	0.040455141
ssh-simplified/s3_clnt_3_true.cil.ll/7039.smt2	2.01353728	0.042987245
ssh-simplified/s3_clnt_3_true.cil.ll/7985.smt2	2.549520393	0.03712581
ssh-simplified/s3_clnt_3_true.cil.ll/9311.smt2	4.435520112	0.04363411
ssh-simplified/s3_clnt_4_true.cil.ll/10355.smt2	1.2218081	0.031278726
ssh-simplified/s3_clnt_4_true.cil.ll/10744.smt2	1.991213842	0.036473479
ssh-simplified/s3_clnt_4_true.cil.ll/10864.smt2	5.658701445	0.045794289
ssh-simplified/s3_clnt_4_true.cil.ll/11251.smt2	2.281675222	0.03727557
ssh-simplified/s3_clnt_4_true.cil.ll/12873.smt2	3.285250526	0.047042041
ssh-simplified/s3_clnt_4_true.cil.ll/13737.smt2	2.526528196	0.047108474
ssh-simplified/s3_clnt_4_true.cil.ll/15272.smt2	2.065188697	0.039468828
ssh-simplified/s3_clnt_4_true.cil.ll/3396.smt2	1.2535477	0.047227486
ssh-simplified/s3_clnt_4_true.cil.ll/5580.smt2	2.79221249	0.048431892
ssh-simplified/s3_clnt_4_true.cil.ll/7587.smt2	5.82979373	0.041857094
ssh-simplified/s3_clnt_4_true.cil.ll/7820.smt2	6.200987061	0.045189165
ssh-simplified/s3_clnt_4_true.cil.ll/8184.smt2	3.568597751	0.050757432
ssh-simplified/s3_srvr_1_false.cil.ll/1.smt2	900	0.067793164
ssh-simplified/s3_srvr_1_true.cil.ll/1209.smt2	900	0.074726488
ssh-simplified/s3_srvr_1_true.cil.ll/131.smt2	0.898668636	0.057677468
ssh-simplified/s3_srvr_1_true.cil.ll/1526.smt2	1.621876877	0.080550659
ssh-simplified/s3_srvr_1_true.cil.ll/1997.smt2	900	0.071491585
ssh-simplified/s3_srvr_1_true.cil.ll/2031.smt2	2.858660149	0.103752365
ssh-simplified/s3_srvr_1_true.cil.ll/2098.smt2	3.850948346	0.111172884
ssh-simplified/s3_srvr_1_true.cil.ll/2305.smt2	0.996498453	0.299527941
ssh-simplified/s3_srvr_1_true.cil.ll/2671.smt2	2.608028102	0.066047489
ssh-simplified/s3_srvr_1_true.cil.ll/2784.smt2	900	0.133958351
ssh-simplified/s3_srvr_1_true.cil.ll/2901.smt2	5.407670855	0.118840612
ssh-simplified/s3_srvr_1_true.cil.ll/2977.smt2	1.44995851	0.053195253
ssh-simplified/s3_srvr_1_true.cil.ll/3081.smt2	2.082909	0.084014694
ssh-simplified/s3_srvr_1_true.cil.ll/3422.smt2	900	0.13479005
ssh-simplified/s3_srvr_1_true.cil.ll/3485.smt2	1.391144268	0.345775994
ssh-simplified/s3_srvr_1_true.cil.ll/460.smt2	900	0.074275469
ssh-simplified/s3_srvr_1_true.cil.ll/786.smt2	1.14334396	0.094642007
ssh-simplified/s3_srvr_1_true.cil.ll/939.smt2	900	0.07108157
ssh-simplified/s3_srvr_1_true.cil.ll/996.smt2	900	0.094267231
ssh-simplified/s3_srvr_11_false.cil.ll/1071.smt2	373.296652009	0.746579556
ssh-simplified/s3_srvr_11_false.cil.ll/1731.smt2	643.372668021	0.353202701
ssh-simplified/s3_srvr_11_false.cil.ll/1754.smt2	900	1.271845911
ssh-simplified/s3_srvr_11_false.cil.ll/1944.smt2	900	2.561212783
ssh-simplified/s3_srvr_11_false.cil.ll/2040.smt2	62.897583579	0.098429303
ssh-simplified/s3_srvr_11_false.cil.ll/2143.smt2	855.647831847	1.075204154
ssh-simplified/s3_srvr_11_false.cil.ll/2262.smt2	329.328327014	0.490769896
ssh-simplified/s3_srvr_11_false.cil.ll/2294.smt2	900	5.111801701
ssh-simplified/s3_srvr_11_false.cil.ll/2510.smt2	115.490145868	0.103053892
ssh-simplified/s3_srvr_11_false.cil.ll/262.smt2	1.285929646	0.066394815
ssh-simplified/s3_srvr_11_false.cil.ll/2632.smt2	900	1.391087756
ssh-simplified/s3_srvr_11_false.cil.ll/307.smt2	1.337397755	0.056259951
ssh-simplified/s3_srvr_11_false.cil.ll/335.smt2	1.075774231	0.056703916
ssh-simplified/s3_srvr_11_false.cil.ll/471.smt2	32.830017561	0.375042981
ssh-simplified/s3_srvr_11_false.cil.ll/827.smt2	15.705781309	0.071165165
ssh-simplified/s3_srvr_11_false.cil.ll/852.smt2	243.673244827	1.382554075
ssh-simplified/s3_srvr_11_false.cil.ll/861.smt2	14.260746343	0.059961723
ssh-simplified/s3_srvr_12_false.cil.ll/10139.smt2	612.152425683	0.085941686
ssh-simplified/s3_srvr_12_false.cil.ll/11393.smt2	171.781252464	0.062807445
ssh-simplified/s3_srvr_12_false.cil.ll/11433.smt2	396.89877646	0.088179688
ssh-simplified/s3_srvr_12_false.cil.ll/1315.smt2	3.707055611	0.050235
ssh-simplified/s3_srvr_12_false.cil.ll/2014.smt2	6.370735013	0.051118066
ssh-simplified/s3_srvr_12_false.cil.ll/2413.smt2	6.185815108	0.050674798
ssh-simplified/s3_srvr_12_false.cil.ll/2851.smt2	7.154766808	0.054581686
ssh-simplified/s3_srvr_12_false.cil.ll/3360.smt2	14.863973009	0.053649502
ssh-simplified/s3_srvr_12_false.cil.ll/3690.smt2	0.612596107	0.039794865
ssh-simplified/s3_srvr_12_false.cil.ll/3828.smt2	15.765313015	0.056841648
ssh-simplified/s3_srvr_12_false.cil.ll/4313.smt2	900	0.056021364
ssh-simplified/s3_srvr_12_false.cil.ll/4769.smt2	900	0.055762791
ssh-simplified/s3_srvr_12_false.cil.ll/5771.smt2	79.933289784	0.053142208
ssh-simplified/s3_srvr_12_false.cil.ll/6221.smt2	3.224366584	0.039579007
ssh-simplified/s3_srvr_12_false.cil.ll/6258.smt2	41.497612237	0.045037779
ssh-simplified/s3_srvr_12_false.cil.ll/7428.smt2	29.171945179	0.049123191
ssh-simplified/s3_srvr_12_false.cil.ll/7451.smt2	55.163773301	0.050968205
ssh-simplified/s3_srvr_12_false.cil.ll/8170.smt2	533.035166087	0.085732828
ssh-simplified/s3_srvr_12_false.cil.ll/8688.smt2	62.987909555	0.056770688
ssh-simplified/s3_srvr_12_false.cil.ll/8721.smt2	272.767637467	0.087387385
ssh-simplified/s3_srvr_12_false.cil.ll/9205.smt2	36.870766559	0.049096
ssh-simplified/s3_srvr_12_false.cil.ll/9412.smt2	218.946708838	0.087110437
ssh-simplified/s3_srvr_12_false.cil.ll/9805.smt2	118.33424739	0.054241369
ssh-simplified/s3_srvr_12_false.cil.ll/9875.smt2	8.9253583	0.041757195
ssh-simplified/s3_srvr_13_false.cil.ll/1186.smt2	78.383739009	0.183688113
ssh-simplified/s3_srvr_13_false.cil.ll/1612.smt2	77.603932593	0.184946613
ssh-simplified/s3_srvr_13_false.cil.ll/1625.smt2	6.888690304	0.066703329
ssh-simplified/s3_srvr_13_false.cil.ll/1868.smt2	57.197280571	0.18309444
ssh-simplified/s3_srvr_13_false.cil.ll/3202.smt2	19.117726959	0.119056029
ssh-simplified/s3_srvr_13_false.cil.ll/343.smt2	66.691477227	0.184764483
ssh-simplified/s3_srvr_13_false.cil.ll/5064.smt2	63.210919528	0.18400271
ssh-simplified/s3_srvr_13_false.cil.ll/5507.smt2	77.607077452	0.184006295
ssh-simplified/s3_srvr_1b_true.cil.ll/10159.smt2	0.579816599	0.025196072
ssh-simplified/s3_srvr_1b_true.cil.ll/13602.smt2	0.565556736	0.027983911
ssh-simplified/s3_srvr_1b_true.cil.ll/15389.smt2	0.57602327	0.029835067
ssh-simplified/s3_srvr_1b_true.cil.ll/17270.smt2	0.570165336	0.011689977
ssh-simplified/s3_srvr_1b_true.cil.ll/18192.smt2	0.588139358	0.012056034
ssh-simplified/s3_srvr_1b_true.cil.ll/20530.smt2	0.628545812	0.009438887
ssh-simplified/s3_srvr_2_false.cil.ll/209.smt2	900	0.064992364
ssh-simplified/s3_srvr_2_false.cil.ll/21.smt2	900	0.079934273
ssh-simplified/s3_srvr_2_false.cil.ll/308.smt2	1.269148024	0.060781044
ssh-simplified/s3_srvr_2_false.cil.ll/341.smt2	0.781623164	0.081973256
ssh-simplified/s3_srvr_2_false.cil.ll/361.smt2	0.727753183	0.075832516
ssh-simplified/s3_srvr_2_false.cil.ll/43.smt2	0.870848874	0.066139879
ssh-simplified/s3_srvr_2_true.cil.ll/1000.smt2	900	0.102578632
ssh-simplified/s3_srvr_2_true.cil.ll/213.smt2	900	0.064982704
ssh-simplified/s3_srvr_2_true.cil.ll/597.smt2	900	0.076542303
ssh-simplified/s3_srvr_2_true.cil.ll/827.smt2	4.630836949	0.102790202
ssh-simplified/s3_srvr_2_true.cil.ll/853.smt2	4.234157312	0.084035608
ssh-simplified/s3_srvr_2_true.cil.ll/860.smt2	6.590321537	0.118704322
ssh-simplified/s3_srvr_2_true.cil.ll/875.smt2	900	0.059275335
ssh-simplified/s3_srvr_2_true.cil.ll/913.smt2	900	0.075438743
ssh-simplified/s3_srvr_2_true.cil.ll/925.smt2	0.696900679	0.06633462
ssh-simplified/s3_srvr_2_true.cil.ll/977.smt2	0.940921786	0.058719479
ssh-simplified/s3_srvr_2_true.cil.ll/998.smt2	900	0.099007466
ssh-simplified/s3_srvr_3_true.cil.ll/285.smt2	1.102752314	0.080238279
ssh-simplified/s3_srvr_3_true.cil.ll/323.smt2	1.719025394	0.063623244
ssh-simplified/s3_srvr_3_true.cil.ll/337.smt2	900	0.088849186
ssh-simplified/s3_srvr_3_true.cil.ll/339.smt2	0.614800426	0.06457374
ssh-simplified/s3_srvr_3_true.cil.ll/37.smt2	900	0.09003034
ssh-simplified/s3_srvr_3_true.cil.ll/44.smt2	0.931671893	0.063128329
ssh-simplified/s3_srvr_6_true.cil.ll/89.smt2	900	0.05955355
ssh-simplified/s3_srvr_7_true.cil.ll/10.smt2	900	0.075980269
ssh-simplified/s3_srvr_7_true.cil.ll/194.smt2	900	0.063410137
ssh-simplified/s3_srvr_7_true.cil.ll/201.smt2	900	0.067711306
ssh-simplified/s3_srvr_7_true.cil.ll/251.smt2	900	0.084003537
ssh-simplified/s3_srvr_7_true.cil.ll/271.smt2	900	0.07929504
ssh-simplified/s3_srvr_7_true.cil.ll/279.smt2	0.787613734	0.055612081
ssh-simplified/s3_srvr_7_true.cil.ll/287.smt2	0.77088619	0.080245408
ssh-simplified/s3_srvr_7_true.cil.ll/308.smt2	0.801989326	0.079235818
ssh-simplified/s3_srvr_7_true.cil.ll/309.smt2	2.082302599	0.081111508
ssh-simplified/s3_srvr_7_true.cil.ll/319.smt2	0.778764356	0.065219846
ssh-simplified/s3_srvr_7_true.cil.ll/352.smt2	0.726459528	0.085696709
ssh-simplified/s3_srvr_8_true.cil.ll/319.smt2	0.783782074	0.058102289
systemc/kundu_true.cil.ll/11032.smt2	0.734781859	0.025529549
systemc/kundu_true.cil.ll/11482.smt2	1.028599742	0.032340561
systemc/kundu_true.cil.ll/12333.smt2	0.83362532	0.029193163
systemc/kundu_true.cil.ll/2059.smt2	0.643573262	0.035131625
systemc/kundu_true.cil.ll/2155.smt2	0.726331506	0.027157481
systemc/kundu_true.cil.ll/2161.smt2	0.795616229	0.028826837
systemc/kundu_true.cil.ll/2852.smt2	0.801075562	0.033771368
systemc/kundu_true.cil.ll/2943.smt2	0.598479189	0.028619076
systemc/kundu_true.cil.ll/3290.smt2	0.784489789	0.028696232
systemc/kundu_true.cil.ll/3645.smt2	0.853279012	0.026313049
systemc/kundu_true.cil.ll/4022.smt2	0.977306529	0.030830259
systemc/kundu_true.cil.ll/7943.smt2	0.815278117	0.03005196
systemc/kundu_true.cil.ll/8712.smt2	1.437745568	0.026584381
systemc/kundu2_false.cil.ll/7098.smt2	0.543377781	0.035930677
systemc/kundu2_false.cil.ll/8602.smt2	0.579069764	0.034351872
systemc/kundu2_false.cil.ll/8687.smt2	0.54862092	0.035772573
systemc/kundu2_false.cil.ll/9083.smt2	0.704175841	0.045694774
systemc/kundu2_false.cil.ll/9568.smt2	0.711808115	0.033635948
systemc/kundu2_false.cil.ll/9938.smt2	0.534951854	0.033353493
systemc/mem_slave_tlm.2_true.cil.ll/12019.smt2	0.538422431	0.038054438
systemc/mem_slave_tlm.3_true.cil.ll/10077.smt2	0.583305076	0.039937842
systemc/mem_slave_tlm.3_true.cil.ll/10234.smt2	0.548298143	0.037346634
systemc/mem_slave_tlm.3_true.cil.ll/10491.smt2	0.699187338	0.026063879
systemc/mem_slave_tlm.3_true.cil.ll/11782.smt2	0.69879734	0.055752117
systemc/mem_slave_tlm.3_true.cil.ll/13520.smt2	0.785882868	0.044205652
systemc/mem_slave_tlm.3_true.cil.ll/14200.smt2	0.554706807	0.043494732
systemc/mem_slave_tlm.3_true.cil.ll/14422.smt2	0.657541165	0.026679618
systemc/mem_slave_tlm.3_true.cil.ll/7560.smt2	0.583230386	0.033322122
systemc/mem_slave_tlm.3_true.cil.ll/9256.smt2	0.576213066	0.035768066
systemc/mem_slave_tlm.4_true.cil.ll/10395.smt2	0.632787836	0.040390099
systemc/mem_slave_tlm.4_true.cil.ll/12934.smt2	0.769130686	0.035720314
systemc/mem_slave_tlm.4_true.cil.ll/12963.smt2	0.613330297	0.04009663
systemc/mem_slave_tlm.4_true.cil.ll/14120.smt2	0.573011349	0.031718478
systemc/mem_slave_tlm.4_true.cil.ll/14994.smt2	0.837081846	0.03450875
systemc/mem_slave_tlm.4_true.cil.ll/3774.smt2	0.627909922	0.041900409
systemc/mem_slave_tlm.4_true.cil.ll/5571.smt2	0.567784106	0.02509348
systemc/mem_slave_tlm.4_true.cil.ll/8630.smt2	0.748303779	0.0284092
systemc/mem_slave_tlm.4_true.cil.ll/8636.smt2	0.828980526	0.033703799
systemc/mem_slave_tlm.5_true.cil.ll/1072.smt2	0.597505561	0.027404994
systemc/mem_slave_tlm.5_true.cil.ll/11521.smt2	0.861438458	0.039070594
systemc/mem_slave_tlm.5_true.cil.ll/12143.smt2	0.958975642	0.043275369
systemc/mem_slave_tlm.5_true.cil.ll/12653.smt2	0.694530903	0.025675698
systemc/mem_slave_tlm.5_true.cil.ll/12656.smt2	0.747357575	0.025545642
systemc/mem_slave_tlm.5_true.cil.ll/12863.smt2	0.954970735	0.036827185
systemc/mem_slave_tlm.5_true.cil.ll/3190.smt2	0.598521914	0.041965831
systemc/mem_slave_tlm.5_true.cil.ll/3230.smt2	0.794769813	0.042410541
systemc/mem_slave_tlm.5_true.cil.ll/3542.smt2	0.597424897	0.035899653
systemc/mem_slave_tlm.5_true.cil.ll/3544.smt2	0.665992593	0.041382461
systemc/mem_slave_tlm.5_true.cil.ll/3603.smt2	0.779847719	0.036447594
systemc/mem_slave_tlm.5_true.cil.ll/7689.smt2	0.833001466	0.027016349
systemc/mem_slave_tlm.5_true.cil.ll/8112.smt2	0.919052917	0.026188557
systemc/mem_slave_tlm.5_true.cil.ll/8927.smt2	0.919185554	0.046193489
systemc/mem_slave_tlm.5_true.cil.ll/9083.smt2	0.954357177	0.039336421
systemc/pc_sfifo_1_true.cil.ll/1101.smt2	900	0.149968528
systemc/pc_sfifo_1_true.cil.ll/123.smt2	8.539597969	0.129551392
systemc/pc_sfifo_1_true.cil.ll/129.smt2	9.114717981	0.151519089
systemc/pc_sfifo_1_true.cil.ll/138.smt2	9.104917602	0.150095765
systemc/pc_sfifo_1_true.cil.ll/209.smt2	9.562326968	0.130883889
systemc/pc_sfifo_1_true.cil.ll/212.smt2	900	0.157781012
systemc/pc_sfifo_1_true.cil.ll/270.smt2	27.122653904	0.134391058
systemc/pc_sfifo_1_true.cil.ll/304.smt2	37.655566704	0.130632428
systemc/pc_sfifo_1_true.cil.ll/386.smt2	146.904645622	0.135975382
systemc/pc_sfifo_1_true.cil.ll/418.smt2	174.436371014	0.125671735
systemc/pc_sfifo_1_true.cil.ll/420.smt2	184.711090494	0.128519817
systemc/pc_sfifo_1_true.cil.ll/458.smt2	296.511267185	0.131162449
systemc/pc_sfifo_1_true.cil.ll/479.smt2	354.544262089	0.123949895
systemc/pc_sfifo_1_true.cil.ll/486.smt2	900	0.147811814
systemc/pc_sfifo_1_true.cil.ll/587.smt2	740.473238799	0.124083755
systemc/pc_sfifo_1_true.cil.ll/588.smt2	791.218315235	0.119836681
systemc/pc_sfifo_1_true.cil.ll/655.smt2	900	0.127143155
systemc/pc_sfifo_1_true.cil.ll/709.smt2	900	0.126491945
systemc/pc_sfifo_1_true.cil.ll/735.smt2	900	0.127900364
systemc/pc_sfifo_1_true.cil.ll/76.smt2	1.979479513	0.133635778
systemc/pc_sfifo_1_true.cil.ll/769.smt2	479.406505742	0.1466859
systemc/pc_sfifo_1_true.cil.ll/784.smt2	900	0.13475079
systemc/pc_sfifo_1_true.cil.ll/795.smt2	900	0.130385083
systemc/pc_sfifo_1_true.cil.ll/818.smt2	900	0.126956569
systemc/pc_sfifo_1_true.cil.ll/871.smt2	900	0.146882163
systemc/pc_sfifo_2_true.cil.ll/1053.smt2	389.936109764	0.059868405
systemc/pc_sfifo_2_true.cil.ll/111.smt2	0.938040813	0.04827359
systemc/pc_sfifo_2_true.cil.ll/1181.smt2	557.434110841	0.050136295
systemc/pc_sfifo_2_true.cil.ll/1211.smt2	900	0.113756933
systemc/pc_sfifo_2_true.cil.ll/1348.smt2	833.333604753	0.073427765
systemc/pc_sfifo_2_true.cil.ll/1351.smt2	900	0.089830559
systemc/pc_sfifo_2_true.cil.ll/1452.smt2	900	0.112205819
systemc/pc_sfifo_2_true.cil.ll/146.smt2	2.858676786	0.077934695
systemc/pc_sfifo_2_true.cil.ll/178.smt2	900	0.080851243
systemc/pc_sfifo_2_true.cil.ll/206.smt2	3.366477068	0.067281995
systemc/pc_sfifo_2_true.cil.ll/250.smt2	3.375078049	0.071960404
systemc/pc_sfifo_2_true.cil.ll/256.smt2	3.592746952	0.068815918
systemc/pc_sfifo_2_true.cil.ll/267.smt2	11.558535699	0.109637204
systemc/pc_sfifo_2_true.cil.ll/345.smt2	8.562903034	0.047904739
systemc/pc_sfifo_2_true.cil.ll/354.smt2	26.784328944	0.07067763
systemc/pc_sfifo_2_true.cil.ll/463.smt2	29.87402237	0.065846446
systemc/pc_sfifo_2_true.cil.ll/571.smt2	180.39928244	0.043219451
systemc/pc_sfifo_2_true.cil.ll/669.smt2	900	0.049519379
systemc/pc_sfifo_2_true.cil.ll/752.smt2	900	0.052022545
systemc/pc_sfifo_2_true.cil.ll/772.smt2	591.692248272	0.057445819
systemc/pc_sfifo_2_true.cil.ll/793.smt2	559.678013682	0.117333375
systemc/pc_sfifo_2_true.cil.ll/865.smt2	712.742427791	0.118633378
systemc/pc_sfifo_2_true.cil.ll/952.smt2	900	0.127378649
systemc/pc_sfifo_2_true.cil.ll/996.smt2	900	0.113262959
systemc/pc_sfifo_3_true.cil.ll/16119.smt2	1.007974903	0.070911651
systemc/pc_sfifo_3_true.cil.ll/16492.smt2	0.588543069	0.0741137
systemc/pc_sfifo_3_true.cil.ll/17832.smt2	1.061154978	0.071736902
systemc/pc_sfifo_3_true.cil.ll/18591.smt2	0.832634323	0.033282279
systemc/pipeline_false.cil.ll/23.smt2	0.599509871	0.067889299
systemc/pipeline_true.cil.ll/1015.smt2	2.940533174	0.095900957
systemc/pipeline_true.cil.ll/1047.smt2	3.209500503	0.072581797
systemc/pipeline_true.cil.ll/1145.smt2	3.225204436	0.077804824
systemc/pipeline_true.cil.ll/156.smt2	2.737991955	0.070749531
systemc/pipeline_true.cil.ll/1594.smt2	3.79975052	0.071941907
systemc/pipeline_true.cil.ll/2291.smt2	2.923064783	0.076508988
systemc/pipeline_true.cil.ll/2819.smt2	4.55341408	0.085109017
systemc/pipeline_true.cil.ll/291.smt2	2.989271165	0.078379643
systemc/pipeline_true.cil.ll/3067.smt2	4.618815343	0.086222139
systemc/pipeline_true.cil.ll/3092.smt2	3.684396109	0.077860521
systemc/pipeline_true.cil.ll/3187.smt2	4.314595591	0.073374148
systemc/pipeline_true.cil.ll/4264.smt2	4.480639831	0.085834731
systemc/pipeline_true.cil.ll/4363.smt2	3.983846245	0.086061644
systemc/pipeline_true.cil.ll/4437.smt2	4.804677717	0.077389807
systemc/pipeline_true.cil.ll/4787.smt2	4.11597496	0.067097197
systemc/pipeline_true.cil.ll/4788.smt2	4.232627314	0.078083873
systemc/pipeline_true.cil.ll/5693.smt2	3.827696678	0.084413696
systemc/pipeline_true.cil.ll/6053.smt2	3.779842519	0.075369024
systemc/pipeline_true.cil.ll/6592.smt2	4.821399199	0.084617313
systemc/pipeline_true.cil.ll/6809.smt2	3.215933989	0.073731072
systemc/pipeline_true.cil.ll/7037.smt2	5.166706022	0.073046713
systemc/pipeline_true.cil.ll/7102.smt2	5.185283149	0.074533197
systemc/pipeline_true.cil.ll/7180.smt2	3.041138792	0.075240702
systemc/pipeline_true.cil.ll/7215.smt2	4.715886215	0.085950028
systemc/pipeline_true.cil.ll/7527.smt2	3.956886225	0.070094269
systemc/token_ring.03_true.cil.ll/9304.smt2	1.461569726	0.048015125
systemc/token_ring.05_false.cil.ll/11902.smt2	900	0.054323856
systemc/token_ring.05_false.cil.ll/173.smt2	900	0.05591077
systemc/token_ring.05_false.cil.ll/18506.smt2	900	0.054299703
systemc/token_ring.05_false.cil.ll/2518.smt2	900	0.058877476
systemc/token_ring.05_false.cil.ll/2912.smt2	900	0.081787868
systemc/token_ring.05_false.cil.ll/3690.smt2	900	0.050610069
systemc/token_ring.05_false.cil.ll/4822.smt2	900	0.068032164
systemc/token_ring.05_true.cil.ll/10541.smt2	900	0.05749971
systemc/token_ring.05_true.cil.ll/11114.smt2	900	0.054165927
systemc/token_ring.05_true.cil.ll/12622.smt2	900	0.057111064
systemc/token_ring.05_true.cil.ll/12645.smt2	900	0.055689975
systemc/token_ring.05_true.cil.ll/15056.smt2	900	0.054463508
systemc/token_ring.05_true.cil.ll/167.smt2	900	0.060008716
systemc/token_ring.05_true.cil.ll/17301.smt2	900	0.053508235
systemc/token_ring.05_true.cil.ll/17869.smt2	900	0.053485817
systemc/token_ring.05_true.cil.ll/231.smt2	900	0.05483839
systemc/token_ring.05_true.cil.ll/2466.smt2	900	0.060929995
systemc/token_ring.05_true.cil.ll/594.smt2	900	0.055479739
systemc/token_ring.05_true.cil.ll/9880.smt2	900	0.054165906
systemc/token_ring.07_false.cil.ll/13782.smt2	0.977374862	0.396982991
systemc/token_ring.07_false.cil.ll/4095.smt2	0.753251006	0.252593887
systemc/token_ring.07_false.cil.ll/8151.smt2	0.550880927	0.045341943
systemc/token_ring.07_true.cil.ll/12304.smt2	1.185577867	0.251919279
systemc/token_ring.07_true.cil.ll/14819.smt2	0.595456603	0.041468818
systemc/token_ring.07_true.cil.ll/15124.smt2	1.220180443	0.255880822
systemc/token_ring.07_true.cil.ll/3851.smt2	0.551123493	0.041553171
systemc/token_ring.07_true.cil.ll/6602.smt2	0.553712099	0.042559032
systemc/token_ring.07_true.cil.ll/7189.smt2	0.558355396	0.04155144
systemc/token_ring.07_true.cil.ll/9240.smt2	2.460586279	0.044575212
systemc/token_ring.08_false.cil.ll/10687.smt2	9.403764307	0.042177342
systemc/token_ring.08_false.cil.ll/10918.smt2	1.152769249	0.285080566
systemc/token_ring.08_false.cil.ll/12182.smt2	1.31427269	0.285256311
systemc/token_ring.08_false.cil.ll/12406.smt2	0.712874621	0.043805514
systemc/token_ring.08_false.cil.ll/13973.smt2	0.702972312	0.042707322
systemc/token_ring.08_false.cil.ll/15218.smt2	0.584178494	0.047168009
systemc/token_ring.08_false.cil.ll/15519.smt2	0.999431014	0.041973104
systemc/token_ring.08_false.cil.ll/6169.smt2	0.713205225	0.044130136
systemc/token_ring.08_false.cil.ll/6671.smt2	1.054090842	0.285443252
systemc/token_ring.08_false.cil.ll/7118.smt2	0.823614511	0.27474981
systemc/token_ring.08_false.cil.ll/751.smt2	2.910715936	0.039825474
systemc/token_ring.08_true.cil.ll/11556.smt2	0.708311941	0.040989382
systemc/token_ring.08_true.cil.ll/15415.smt2	11.245686944	0.047874914
systemc/token_ring.08_true.cil.ll/15453.smt2	0.552678823	0.047806871
systemc/token_ring.08_true.cil.ll/15679.smt2	0.991991199	0.275558346
systemc/token_ring.08_true.cil.ll/15830.smt2	0.771672875	0.265052832
systemc/token_ring.08_true.cil.ll/16566.smt2	1.221981863	0.034973795
systemc/token_ring.08_true.cil.ll/181.smt2	2.937375447	0.046111977
systemc/token_ring.08_true.cil.ll/8751.smt2	0.549681357	0.036262044
systemc/token_ring.09_false.cil.ll/10280.smt2	900	0.058202761
systemc/token_ring.09_false.cil.ll/10296.smt2	900	0.061807557
systemc/token_ring.09_false.cil.ll/10299.smt2	900	0.05792178
systemc/token_ring.09_false.cil.ll/12673.smt2	900	0.054989374
systemc/token_ring.09_false.cil.ll/1843.smt2	900	0.052609196
systemc/token_ring.09_false.cil.ll/2061.smt2	900	0.05167771
systemc/token_ring.09_false.cil.ll/2353.smt2	900	0.054797573
systemc/token_ring.09_false.cil.ll/2899.smt2	900	0.055117211
systemc/token_ring.09_false.cil.ll/3889.smt2	900	0.05995235
systemc/token_ring.09_false.cil.ll/4559.smt2	900	0.051377199
systemc/token_ring.09_false.cil.ll/4707.smt2	900	0.059083857
systemc/token_ring.09_false.cil.ll/4716.smt2	900	0.055827986
systemc/token_ring.09_false.cil.ll/6169.smt2	900	0.053512809
systemc/token_ring.09_false.cil.ll/6351.smt2	900	0.050931703
systemc/token_ring.09_false.cil.ll/6802.smt2	900	0.050951654
systemc/token_ring.09_false.cil.ll/731.smt2	900	0.055898869
systemc/token_ring.09_false.cil.ll/7993.smt2	900	0.050801741
systemc/token_ring.09_true.cil.ll/10222.smt2	900	0.054703369
systemc/token_ring.09_true.cil.ll/1102.smt2	900	0.051463728
systemc/token_ring.09_true.cil.ll/12510.smt2	900	0.053246015
systemc/token_ring.09_true.cil.ll/12597.smt2	900	0.051131103
systemc/token_ring.09_true.cil.ll/13105.smt2	900	0.053696728
systemc/token_ring.09_true.cil.ll/13204.smt2	900	0.054589172
systemc/token_ring.09_true.cil.ll/13286.smt2	900	0.050656768
systemc/token_ring.09_true.cil.ll/1800.smt2	900	0.059175472
systemc/token_ring.09_true.cil.ll/5787.smt2	900	0.054819767
systemc/token_ring.09_true.cil.ll/6321.smt2	900	0.050826021
systemc/token_ring.09_true.cil.ll/6411.smt2	900	0.0598803
systemc/token_ring.09_true.cil.ll/6914.smt2	900	0.051393168
systemc/token_ring.09_true.cil.ll/714.smt2	900	0.059982383
systemc/token_ring.09_true.cil.ll/7347.smt2	900	0.055401434
systemc/token_ring.09_true.cil.ll/8475.smt2	900	0.058392909
systemc/token_ring.09_true.cil.ll/9343.smt2	900	0.054465136
systemc/token_ring.09_true.cil.ll/94.smt2	900	0.05537666
systemc/token_ring.09_true.cil.ll/9648.smt2	900	0.055097086
systemc/token_ring.09_true.cil.ll/9656.smt2	900	0.053429277
systemc/token_ring.11_false.cil.ll/1191.smt2	11.613398791	0.03406626
systemc/token_ring.11_false.cil.ll/12169.smt2	1.361045135	0.265526807
systemc/token_ring.11_false.cil.ll/13231.smt2	11.616662548	0.043957839
systemc/token_ring.11_false.cil.ll/16074.smt2	11.653862254	0.047132847
systemc/token_ring.11_false.cil.ll/1992.smt2	0.546496062	0.043798641
systemc/token_ring.11_false.cil.ll/2055.smt2	1.158972599	0.268773797
systemc/token_ring.11_false.cil.ll/3626.smt2	1.751807648	0.26344983
systemc/token_ring.11_false.cil.ll/4033.smt2	1.156556301	0.257619905
systemc/token_ring.11_false.cil.ll/5289.smt2	22.141524088	0.044321022
systemc/token_ring.11_false.cil.ll/7932.smt2	11.661972331	0.039741883
systemc/token_ring.11_false.cil.ll/869.smt2	1.600334181	0.635424272
systemc/token_ring.11_false.cil.ll/8865.smt2	0.622310445	0.046783477
systemc/token_ring.11_false.cil.ll/9519.smt2	1.417081025	0.632462332
systemc/token_ring.11_false.cil.ll/9841.smt2	1.114619989	0.039982079
systemc/token_ring.11_true.cil.ll/1173.smt2	11.745163902	0.03925131
systemc/token_ring.11_true.cil.ll/12281.smt2	1.385445607	0.634168446
systemc/token_ring.11_true.cil.ll/12741.smt2	1.236547598	0.039422837
systemc/token_ring.11_true.cil.ll/13743.smt2	1.705559287	0.629530235
systemc/token_ring.11_true.cil.ll/14221.smt2	0.589053155	0.039864981
systemc/token_ring.11_true.cil.ll/15278.smt2	2.233531197	0.256690087
systemc/token_ring.11_true.cil.ll/1831.smt2	1.391583703	0.259389539
systemc/token_ring.11_true.cil.ll/2072.smt2	2.121158928	0.259287643
systemc/token_ring.11_true.cil.ll/329.smt2	1.351501848	0.259102506
systemc/token_ring.11_true.cil.ll/3930.smt2	9.443355081	0.040683261
systemc/token_ring.11_true.cil.ll/6244.smt2	1.85601612	0.627807007
systemc/token_ring.13_false.cil.ll/10077.smt2	1.223700658	0.044741841
systemc/token_ring.13_false.cil.ll/11327.smt2	1.128135281	0.044045629
systemc/token_ring.13_false.cil.ll/1242.smt2	0.746606661	0.045920196
systemc/token_ring.13_false.cil.ll/12614.smt2	1.059310686	0.047220553
systemc/token_ring.13_false.cil.ll/12911.smt2	1.306239785	0.038950144
systemc/token_ring.13_false.cil.ll/13819.smt2	0.746395744	0.047232863
systemc/token_ring.13_false.cil.ll/2424.smt2	4.857606787	0.538647359
systemc/token_ring.13_false.cil.ll/2951.smt2	1.171958365	0.047661636
systemc/token_ring.13_false.cil.ll/4311.smt2	1.415631808	0.502389754
systemc/token_ring.13_false.cil.ll/5734.smt2	1.169858816	0.041883226
systemc/token_ring.13_false.cil.ll/6639.smt2	0.548872532	0.046671145
systemc/token_ring.13_false.cil.ll/7706.smt2	1.512518737	0.49705257
systemc/token_ring.13_false.cil.ll/7874.smt2	1.520671234	0.049341129
systemc/token_ring.13_false.cil.ll/8425.smt2	0.627303251	0.048037647
systemc/token_ring.13_false.cil.ll/9401.smt2	1.278144336	0.499008858
systemc/token_ring.13_true.cil.ll/10038.smt2	1.698351457	0.042139534
systemc/token_ring.13_true.cil.ll/11503.smt2	0.698038305	0.046139484
systemc/token_ring.13_true.cil.ll/11553.smt2	1.218608668	0.045472091
systemc/token_ring.13_true.cil.ll/11679.smt2	1.769451796	0.047354674
systemc/token_ring.13_true.cil.ll/12836.smt2	1.814790874	0.045145113
systemc/token_ring.13_true.cil.ll/1916.smt2	2.901769448	0.499721274
systemc/token_ring.13_true.cil.ll/2477.smt2	0.745649915	0.041766086
systemc/token_ring.13_true.cil.ll/4041.smt2	0.750216787	0.047263451
systemc/token_ring.13_true.cil.ll/4297.smt2	2.122301783	0.546049455
systemc/token_ring.13_true.cil.ll/4372.smt2	2.928723822	0.500918717
systemc/token_ring.13_true.cil.ll/4735.smt2	0.621445577	0.050081329
systemc/token_ring.13_true.cil.ll/4987.smt2	1.348075942	0.539800355
systemc/token_ring.13_true.cil.ll/6842.smt2	0.746753262	0.051950405
systemc/token_ring.13_true.cil.ll/7864.smt2	1.128909705	0.051545187
systemc/token_ring.13_true.cil.ll/8712.smt2	0.609477686	0.047586887
systemc/token_ring.15_false.cil.ll/10901.smt2	0.679552113	0.046173388
systemc/token_ring.15_false.cil.ll/11958.smt2	1.78411018	0.498834528
systemc/token_ring.15_false.cil.ll/14124.smt2	1.454219948	0.50117216
systemc/token_ring.15_false.cil.ll/14437.smt2	1.080102055	0.047302341
systemc/token_ring.15_false.cil.ll/14518.smt2	1.823257271	0.040467485
systemc/token_ring.15_false.cil.ll/2084.smt2	0.752282248	0.040999772
systemc/token_ring.15_false.cil.ll/3350.smt2	2.929668566	0.496814228
systemc/token_ring.15_false.cil.ll/4173.smt2	1.149271011	0.535157403
systemc/token_ring.15_false.cil.ll/5072.smt2	0.743699861	0.048435939
systemc/token_ring.15_false.cil.ll/6410.smt2	3.227280033	0.530746165
systemc/token_ring.15_false.cil.ll/7780.smt2	0.698537329	0.04479568
systemc/token_ring.15_false.cil.ll/8106.smt2	1.608199887	0.046957985
systemc/token_ring.15_false.cil.ll/8928.smt2	1.542122241	0.537125198
systemc/toy_true.cil.ll/1016.smt2	6.726402295	0.0137253
systemc/toy_true.cil.ll/1037.smt2	900	0.093883617
systemc/toy_true.cil.ll/1049.smt2	900	0.031526449
systemc/toy_true.cil.ll/1052.smt2	900	0.031367656
systemc/toy_true.cil.ll/1091.smt2	7.404528702	0.015706398
systemc/toy_true.cil.ll/1171.smt2	900	0.097818717
systemc/toy_true.cil.ll/1289.smt2	900	0.10138225
systemc/toy_true.cil.ll/166.smt2	2.519296867	0.029321563
systemc/toy_true.cil.ll/203.smt2	0.575588123	0.012837506
systemc/toy_true.cil.ll/288.smt2	13.854541327	0.031985917
systemc/toy_true.cil.ll/346.smt2	40.748833168	0.081814815
systemc/toy_true.cil.ll/480.smt2	215.430540491	0.0817427
systemc/toy_true.cil.ll/546.smt2	3.306311868	0.014632402
systemc/toy_true.cil.ll/563.smt2	3.30530295	0.016263068
systemc/toy_true.cil.ll/601.smt2	333.982438411	0.044263618
systemc/toy_true.cil.ll/641.smt2	459.825167562	0.032411937
systemc/toy_true.cil.ll/736.smt2	700.159352003	0.090491005
systemc/toy_true.cil.ll/771.smt2	697.141220198	0.088310924
systemc/toy_true.cil.ll/820.smt2	695.682000427	0.028050022
systemc/toy_true.cil.ll/832.smt2	782.329698594	0.092044497
systemc/toy_true.cil.ll/843.smt2	788.231497008	0.097712436
systemc/toy_true.cil.ll/856.smt2	900	0.086568459
systemc/toy_true.cil.ll/911.smt2	900	0.07868289
systemc/toy_true.cil.ll/912.smt2	900	0.09673542
systemc/toy_true.cil.ll/949.smt2	900	0.030134752
systemc/transmitter.06_false.cil.ll/8331.smt2	0.578258252	0.033504783
systemc/transmitter.06_false.cil.ll/9324.smt2	0.576857143	0.031640716
systemc/transmitter.07_false.cil.ll/18326.smt2	0.62474828	0.030755263
systemc/transmitter.09_false.cil.ll/5.smt2	0.67185371	0.160259615
systemc/transmitter.10_false.cil.ll/10148.smt2	0.736975837	0.031998186
systemc/transmitter.10_false.cil.ll/13225.smt2	0.721709394	0.034271693
systemc/transmitter.10_false.cil.ll/13584.smt2	0.82253645	0.037498859
systemc/transmitter.10_false.cil.ll/9304.smt2	0.684982344	0.032785251
systemc/transmitter.11_false.cil.ll/11774.smt2	0.563034666	0.031149715
systemc/transmitter.12_false.cil.ll/12202.smt2	0.606517225	0.03303316
systemc/transmitter.12_false.cil.ll/7410.smt2	0.683981601	0.029407594
systemc/transmitter.12_false.cil.ll/8135.smt2	0.551339146	0.031691608
systemc/transmitter.13_false.cil.ll/11289.smt2	0.656028855	0.034532761
systemc/transmitter.13_false.cil.ll/11567.smt2	0.726790021	0.034567881
systemc/transmitter.13_false.cil.ll/12722.smt2	0.980008548	0.039544661
systemc/transmitter.13_false.cil.ll/14011.smt2	0.773552049	0.037594356
systemc/transmitter.13_false.cil.ll/9620.smt2	0.555665646	0.037991362

4 Simplification times

We now explore the times taken by simplifications.

simplTimes.smtlib <- read.csv("simpltimes_smtlib.csv", header=TRUE, stringsAsFactors=FALSE)
simplTimes.symdivine <- read.csv("simpltimes_symdivine.csv", header=TRUE, stringsAsFactors=FALSE)
simplTimes <- rbind(simplTimes.smtlib, simplTimes.symdivine)

The mean simplification time:

mean(simplTimes$simpltime)

0.0328274277724841

The maximum simplification time:

max(simplTimes$simpltime)

1.29348106891848

5 Data files

Files containing all used benchmarks and all measured results are available below.

On Simplification of Formulas with Unconstrained Variables and Quantifiers

Table of Contents

1 Z3

1.1 SMT-LIB

1.1.1 Load the results

1.1.2 Result counts

1.1.3 Total time/memory

1.1.4 Scatter plots

1.1.5 Quantile plot

1.1.6 Degraded performance

1.1.7 Improved performance

1.2 SymDIVINE

1.2.1 Load the results

1.2.2 Result counts

1.2.3 Total time/memory

1.2.4 Scatter plots

1.2.5 Memory

1.2.6 Quantile plot

1.2.7 Degraded performance

1.2.8 Improved performance

2 Q3B

2.1 SMT-LIB

2.1.1 Load the results

2.1.2 Result counts

2.1.3 Total time/memory

2.1.4 Scatter plots

2.1.5 Quantile plot

2.1.6 Degraded performance

2.1.7 Improved performance

2.2 SymDIVINE

2.2.1 Load the results

2.2.2 Result counts

2.2.3 Total time/memory

2.2.4 Scatter plots

2.2.5 Quantile plot

2.2.6 Degraded performance

2.2.7 Improved performance

3 Boolector

3.1 SMT-LIB

3.1.1 Load the results

3.1.2 Result counts

3.1.3 Total time/memory

3.1.4 Scatter plots

3.1.5 Quantile plot

3.1.6 Degraded performance

3.1.7 Improved performance

3.2 SymDIVINE

3.2.1 Load the results

3.2.2 Result counts

3.2.3 Total time/memory

3.2.4 Scatter plots

3.2.5 Memory

3.2.6 Quantile plot

3.2.7 Degraded performance

3.2.8 Improved performance

4 Simplification times

5 Data files

5.1 Benchmark files

5.2 SMT-LIB results

5.3 SymDIVINE results

5.4 Simplificationt times