about summary refs log tree commit diff homepage
path: root/test/Feature
diff options
context:
space:
mode:
Diffstat (limited to 'test/Feature')
-rw-r--r--test/Feature/CopyOnWrite.c2
-rw-r--r--test/Feature/MakeSymbolicName.c2
-rw-r--r--test/Feature/Searchers.c31
3 files changed, 19 insertions, 16 deletions
diff --git a/test/Feature/CopyOnWrite.c b/test/Feature/CopyOnWrite.c
index ee3ea15e..ce77c802 100644
--- a/test/Feature/CopyOnWrite.c
+++ b/test/Feature/CopyOnWrite.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
-// RUN: %klee --use-random-search --exit-on-error %t1.bc
+// RUN: %klee --search=random-state --exit-on-error %t1.bc
 
 #include <assert.h>
 
diff --git a/test/Feature/MakeSymbolicName.c b/test/Feature/MakeSymbolicName.c
index a4d4e2a6..a31b4a9b 100644
--- a/test/Feature/MakeSymbolicName.c
+++ b/test/Feature/MakeSymbolicName.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
-// RUN: %klee --use-random-search --exit-on-error %t1.bc
+// RUN: %klee --search=random-state --exit-on-error %t1.bc
 
 #include <assert.h>
 
diff --git a/test/Feature/Searchers.c b/test/Feature/Searchers.c
index d61037b9..b120d354 100644
--- a/test/Feature/Searchers.c
+++ b/test/Feature/Searchers.c
@@ -1,27 +1,30 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
 // RUN: %klee %t2.bc
-// RUN: %klee --use-random-search %t2.bc
-// RUN: %klee --use-non-uniform-random-search %t2.bc
-// RUN: %klee --use-non-uniform-random-search --weight-type=query-cost %t2.bc
+// RUN: %klee --search=random-state %t2.bc
+// RUN: %klee --search=nurs:depth %t2.bc
+// RUN: %klee --search=nurs:qc %t2.bc
 // RUN: %klee --use-batching-search %t2.bc
-// RUN: %klee --use-batching-search --use-random-search %t2.bc
-// RUN: %klee --use-batching-search --use-non-uniform-random-search %t2.bc
-// RUN: %klee --use-batching-search --use-non-uniform-random-search --weight-type=query-cost %t2.bc
-// RUN: %klee --use-merge --debug-log-merge --debug-log-state-merge %t2.bc
-// RUN: %klee --use-merge --use-batching-search %t2.bc
-// RUN: %klee --use-merge --use-batching-search --use-random-search %t2.bc
-// RUN: %klee --use-merge --use-batching-search --use-non-uniform-random-search %t2.bc
-// RUN: %klee --use-merge --use-batching-search --use-non-uniform-random-search --weight-type=query-cost %t2.bc
+// RUN: %klee --use-batching-search --search=random-state %t2.bc
+// RUN: %klee --use-batching-search --search=nurs:depth %t2.bc
+// RUN: %klee --use-batching-search --search=nurs:qc %t2.bc
+// RUN: %klee --search=random-path --search=nurs:qc %t2.bc
+// RUN: %klee --use-merge --search=dfs --debug-log-merge --debug-log-state-merge %t2.bc
+// RUN: %klee --use-merge --use-batching-search --search=dfs %t2.bc
+// RUN: %klee --use-merge --use-batching-search --search=random-state %t2.bc
+// RUN: %klee --use-merge --use-batching-search --search=nurs:depth %t2.bc
+// RUN: %klee --use-merge --use-batching-search --search=nurs:qc %t2.bc
 // RUN: %klee --use-iterative-deepening-time-search --use-batching-search %t2.bc
-// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --use-random-search %t2.bc
-// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --use-non-uniform-random-search %t2.bc
-// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --use-non-uniform-random-search --weight-type=query-cost %t2.bc
+// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --search=random-state %t2.bc
+// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --search=nurs:depth %t2.bc
+// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --search=nurs:qc %t2.bc
 
 
 /* this test is basically just for coverage and doesn't really do any
    correctness check (aside from testing that the various combinations
    don't crash) */
 
+#include <stdlib.h>
+
 int validate(char *buf, int N) {
 
   int i;