update last set of experimental results

gernst · Oct 12, 2023 · 259f3dd · 259f3dd
1 parent 0af170d
commit 259f3dd
Show file tree

Hide file tree

Showing 11 changed files with 3,881 additions and 294 deletions.
diff --git a/Makefile b/Makefile
@@ -46,7 +46,7 @@ thesy: $T
 
 all: $S $C $E $T
 
-TEX = $(SMALL:%.bpl=%.tex)
+TEX = $(BPL:%.bpl=%.tex)
 tex: $(TEX)
 
 %.tex: %.bpl %.structural.bpl %.conditional.bpl %.enumerate.bpl %.th.log

diff --git a/cuvee/src/cuvee/TACAS.scala b/cuvee/src/cuvee/TACAS.scala
@@ -13,7 +13,7 @@ object TACAS {
 
     val (cmds, st) = parse(basepath + ".bpl")
 
-    implicit val solver = Solver.z3(100)
+    implicit val solver = Solver.z3(500)
     // Solver.debug = true
 
     for (cmd <- cmds)

diff --git a/evaluation/lemmas/list.html b/evaluation/lemmas/list.html
diff --git a/evaluation/lemmas/list.md b/evaluation/lemmas/list.md
diff --git a/evaluation/lemmas/list.tex b/evaluation/lemmas/list.tex
@@ -9,47 +9,47 @@
 \newcommand{\xE}{32}
 \newcommand{\xF}{33}
 
-\newcommand{\xG}{6}
-\newcommand{\xH}{8}
-\newcommand{\xI}{9}
+\newcommand{\xG}{7}
+\newcommand{\xH}{10}
+\newcommand{\xI}{11}
 
 \newcommand{\xJ}{1}
 \newcommand{\xK}{2}
 \newcommand{\xL}{3}
 
 
 % group: conditional
-\newcommand{\yA}{28}
+\newcommand{\yA}{30}
 \newcommand{\yB}{50}
 \newcommand{\yC}{52}
 
-\newcommand{\yD}{22}
+\newcommand{\yD}{21}
 \newcommand{\yE}{32}
 \newcommand{\yF}{34}
 
-\newcommand{\yG}{6}
-\newcommand{\yH}{9}
-\newcommand{\yI}{11}
+\newcommand{\yG}{7}
+\newcommand{\yH}{10}
+\newcommand{\yI}{12}
 
 \newcommand{\yJ}{1}
 \newcommand{\yK}{2}
 \newcommand{\yL}{4}
 
 
 % group: enumerate
-\newcommand{\zA}{27}
+\newcommand{\zA}{24}
 \newcommand{\zB}{28}
 \newcommand{\zC}{31}
 
-\newcommand{\zD}{15}
-\newcommand{\zE}{13}
+\newcommand{\zD}{12}
+\newcommand{\zE}{14}
 \newcommand{\zF}{15}
 
-\newcommand{\zG}{13}
-\newcommand{\zH}{12}
-\newcommand{\zI}{14}
+\newcommand{\zG}{12}
+\newcommand{\zH}{13}
+\newcommand{\zI}{13}
 
-\newcommand{\zJ}{5}
+\newcommand{\zJ}{2}
 \newcommand{\zK}{2}
 \newcommand{\zL}{5}
 
@@ -60,15 +60,15 @@
 \newcommand{\wC}{6}
 
 \newcommand{\wD}{2}
-\newcommand{\wE}{1}
-\newcommand{\wF}{6}
+\newcommand{\wE}{3}
+\newcommand{\wF}{5}
 
-\newcommand{\wG}{1}
+\newcommand{\wG}{2}
 \newcommand{\wH}{3}
 \newcommand{\wI}{6}
 
 \newcommand{\wJ}{1}
 \newcommand{\wK}{1}
-\newcommand{\wL}{3}
+\newcommand{\wL}{5}
 
 
diff --git a/evaluation/lemmas/nat.html b/evaluation/lemmas/nat.html
diff --git a/evaluation/lemmas/nat.md b/evaluation/lemmas/nat.md
diff --git a/evaluation/lemmas/nat.tex b/evaluation/lemmas/nat.tex
@@ -6,7 +6,7 @@
 \newcommand{\xC}{10}
 
 \newcommand{\xD}{7}
-\newcommand{\xE}{9}
+\newcommand{\xE}{8}
 \newcommand{\xF}{10}
 
 \newcommand{\xG}{2}
@@ -19,56 +19,56 @@
 
 
 % group: conditional
-\newcommand{\yA}{32}
-\newcommand{\yB}{44}
+\newcommand{\yA}{34}
+\newcommand{\yB}{43}
 \newcommand{\yC}{45}
 
 \newcommand{\yD}{7}
-\newcommand{\yE}{9}
+\newcommand{\yE}{8}
 \newcommand{\yF}{10}
 
 \newcommand{\yG}{2}
 \newcommand{\yH}{2}
 \newcommand{\yI}{4}
 
 \newcommand{\yJ}{2}
-\newcommand{\yK}{3}
+\newcommand{\yK}{2}
 \newcommand{\yL}{4}
 
 
 % group: enumerate
-\newcommand{\zA}{50}
-\newcommand{\zB}{153}
+\newcommand{\zA}{49}
+\newcommand{\zB}{150}
 \newcommand{\zC}{159}
 
 \newcommand{\zD}{13}
-\newcommand{\zE}{58}
+\newcommand{\zE}{55}
 \newcommand{\zF}{64}
 
-\newcommand{\zG}{14}
-\newcommand{\zH}{60}
+\newcommand{\zG}{13}
+\newcommand{\zH}{55}
 \newcommand{\zI}{64}
 
-\newcommand{\zJ}{37}
-\newcommand{\zK}{104}
+\newcommand{\zJ}{30}
+\newcommand{\zK}{102}
 \newcommand{\zL}{111}
 
 
 % group: thesy
 \newcommand{\wA}{34}
-\newcommand{\wB}{49}
+\newcommand{\wB}{51}
 \newcommand{\wC}{59}
 
-\newcommand{\wD}{3}
-\newcommand{\wE}{6}
+\newcommand{\wD}{4}
+\newcommand{\wE}{7}
 \newcommand{\wF}{12}
 
-\newcommand{\wG}{10}
-\newcommand{\wH}{14}
-\newcommand{\wI}{21}
+\newcommand{\wG}{11}
+\newcommand{\wH}{16}
+\newcommand{\wI}{22}
 
-\newcommand{\wJ}{4}
-\newcommand{\wK}{8}
-\newcommand{\wL}{8}
+\newcommand{\wJ}{6}
+\newcommand{\wK}{9}
+\newcommand{\wL}{9}