update btor2 files

cksystemsgroup · Nov 23, 2023 · d55abc8 · d55abc8
1 parent 86e58eb
commit d55abc8
Show file tree

Hide file tree

Showing 35 changed files with 43,573 additions and 764,032 deletions.
diff --git a/lion/benchmarks/insertion-sort-il9.btor2 b/lion/benchmarks/insertion-sort-il9.btor2
diff --git a/lion/benchmarks/microbenchmark-il0.btor2 b/lion/benchmarks/microbenchmark-il0.btor2
diff --git a/lion/benchmarks/microbenchmark-il1.btor2 b/lion/benchmarks/microbenchmark-il1.btor2
diff --git a/lion/benchmarks/microbenchmark-il2.btor2 b/lion/benchmarks/microbenchmark-il2.btor2
diff --git a/lion/benchmarks/microbenchmark-il3.btor2 b/lion/benchmarks/microbenchmark-il3.btor2
diff --git a/lion/benchmarks/microbenchmark-il4.btor2 b/lion/benchmarks/microbenchmark-il4.btor2
diff --git a/lion/benchmarks/microbenchmark-il5.btor2 b/lion/benchmarks/microbenchmark-il5.btor2
diff --git a/lion/benchmarks/microbenchmark-il6.btor2 b/lion/benchmarks/microbenchmark-il6.btor2
diff --git a/lion/benchmarks/microbenchmark-il7.btor2 b/lion/benchmarks/microbenchmark-il7.btor2
diff --git a/lion/benchmarks/microbenchmark-il8.btor2 b/lion/benchmarks/microbenchmark-il8.btor2
diff --git a/lion/benchmarks/produce-btor2-files.sh b/lion/benchmarks/produce-btor2-files.sh
@@ -1,36 +1,26 @@
 #!/bin/bash
 
-selfie -c ../../tools/cstar-lib.c tiny-program-good-performance.c -o tiny-program-good-performance.m
+time (gtimeout --foreground -v 35m ../../target/release/unicorn beator tiny-program-good-performance.m --solver z3 --input-limit 2 -t 200000 --one-query -v error --out tiny-program-good-performance-il2.btor2)
 
-selfie -c ../../tools/cstar-lib.c tiny-program-bad-performance.c -o tiny-program-bad-performance.m
-
-selfie -c insertion-sort.c -o insertion-sort.m
-
-selfie -c ../../tools/cstar-lib.c reservoir-sampling.c -o reservoir-sampling.m
-
-selfie -c ../../tools/cstar-lib.c reservoir-sampling-constant-workload.c -o reservoir-sampling-constant-workload.m
-
-time (gtimeout --foreground -v 35m ../../target/release/unicorn beator tiny-program-good-performance.m --unroll 0 --solver z3 --input-limit 2 -t 200000 --one-query -v error --out tiny-program-good-performance-il2.btor2)
-
-time (gtimeout --foreground -v 35m ../../target/release/unicorn beator tiny-program-bad-performance.m --unroll 0 --solver z3 --input-limit 2 -t 200000 --one-query -v error --out tiny-program-good-performance-il2.btor2)
+time (gtimeout --foreground -v 35m ../../target/release/unicorn beator tiny-program-bad-performance.m --solver z3 --input-limit 2 -t 200000 --one-query -v error --out tiny-program-good-performance-il2.btor2)
 
 i=0
 
 while [ $i -le 8 ]
 do
   echo "microbenchmark z3 input-limit $i"
-time (gtimeout --foreground -v 35m ../../target/release/unicorn beator microbenchmark.m --unroll 0 --solver z3 --input-limit $i -t 200000 --one-query -v error --out microbenchmark-il${i}.btor2)
+time (gtimeout --foreground -v 35m ../../target/release/unicorn beator microbenchmark.m --solver z3 --input-limit $i -t 200000 --one-query -v error --out microbenchmark-il${i}.btor2)
   ((i += 1))
 done
 
-time (gtimeout --foreground -v 35m ../../target/release/unicorn beator insertion-sort.m --unroll 0 --solver z3 --input-limit 2 -t 200000 --one-query -v error --out insertion-sort-il${i}.btor2)
+time (gtimeout --foreground -v 35m ../../target/release/unicorn beator insertion-sort.m --solver z3 --input-limit 2 -t 200000 --one-query -v error --out insertion-sort-il${i}.btor2)
 
 i=0
 
 while [ $i -le 8 ]
 do
   echo "reservoir-sampling z3 input-limit $i"
-time (gtimeout --foreground -v 35m ../../target/release/unicorn beator reservoir-sampling.m --unroll 0 --solver z3 --input-limit $i -t 200000 --one-query -v error --out reservoir-sampling-il${i}.btor2)
+time (gtimeout --foreground -v 35m ../../target/release/unicorn beator reservoir-sampling.m --solver z3 --input-limit $i -t 200000 --one-query -v error --out reservoir-sampling-il${i}.btor2)
   ((i += 1))
 done
 
@@ -39,6 +29,6 @@ i=0
 while [ $i -le 8 ]
 do
   echo "reservoir-sampling-constant-workload z3 input-limit $i"
-time (gtimeout --foreground -v 35m ../../target/release/unicorn beator reservoir-sampling-constant-workload.m --unroll 0 --solver z3 --input-limit $i -t 200000 --one-query -v error --out reservoir-sampling-constant-workload-il${i}.btor2)
+time (gtimeout --foreground -v 35m ../../target/release/unicorn beator reservoir-sampling-constant-workload.m --solver z3 --input-limit $i -t 200000 --one-query -v error --out reservoir-sampling-constant-workload-il${i}.btor2)
   ((i += 1))
 done