File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 22// REQUIRES: z3
33// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
44// RUN: rm -rf %t.klee-out
5- // RUN: %klee --output-dir=%t.klee-out --solver-backend=stp --use-forked-solver=false --debug-crosscheck-core-solver=z3 %t1.bc 2>&1 | FileCheck %s
5+ // RUN: %klee --output-dir=%t.klee-out --solver-backend=stp --use-forked-solver=false --debug-crosscheck-core-solver=z3 --use-guided-search=none %t1.bc 2>&1 | FileCheck %s
66
77#include "ExerciseSolver.c.inc"
88
9- // CHECK: KLEE: done: completed paths = 9
10- // CHECK: KLEE: done: partially completed paths = 5
9+ // CHECK: KLEE: done: completed paths = 18
10+ // CHECK: KLEE: done: partially completed paths = 0
Original file line number Diff line number Diff line change 11// REQUIRES: z3
22// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
33// RUN: rm -rf %t.klee-out
4- // RUN: %klee --output-dir=%t.klee-out --search=bfs --solver-backend=z3-tree --max-solvers-approx-tree-inc=4 --debug-crosscheck-core-solver=z3 --debug-z3-validate-models --debug-assignment-validating-solver --use-cex-cache=false %t1.bc 2>&1 | FileCheck %s
4+ // RUN: %klee --output-dir=%t.klee-out --search=bfs --solver-backend=z3-tree --max-solvers-approx-tree-inc=4 --debug-crosscheck-core-solver=z3 --debug-z3-validate-models --debug-assignment-validating-solver --use-cex-cache=false --use-guided-search=none %t1.bc 2>&1 | FileCheck %s
55// RUN: rm -rf %t.klee-out
6- // RUN: %klee --output-dir=%t.klee-out --search=dfs --solver-backend=z3-tree --max-solvers-approx-tree-inc=64 --debug-crosscheck-core-solver=z3 --debug-z3-validate-models --debug-assignment-validating-solver --use-cex-cache=false %t1.bc 2>&1 | FileCheck %s
6+ // RUN: %klee --output-dir=%t.klee-out --search=dfs --solver-backend=z3-tree --max-solvers-approx-tree-inc=64 --debug-crosscheck-core-solver=z3 --debug-z3-validate-models --debug-assignment-validating-solver --use-cex-cache=false --use-guided-search=none %t1.bc 2>&1 | FileCheck %s
77
88#include "ExerciseSolver.c.inc"
99
10- // CHECK: KLEE: done: completed paths = 10
11- // CHECK: KLEE: done: partially completed paths = 4
10+ // CHECK: KLEE: done: completed paths = 18
11+ // CHECK: KLEE: done: partially completed paths = 0
Original file line number Diff line number Diff line change 11// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
22// RUN: rm -rf %t.klee-out
3- // RUN: %klee --output-dir=%t.klee-out --solver-backend=dummy %t1.bc 2>&1 | FileCheck %s
3+ // RUN: %klee --output-dir=%t.klee-out --search=bfs -- solver-backend=dummy --use-guided-search=none %t1.bc 2>&1 | FileCheck %s
44
55#include "ExerciseSolver.c.inc"
66
Original file line number Diff line number Diff line change 11// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
22// RUN: rm -rf %t.klee-out
3- // RUN: %klee --output-dir=%t.klee-out --debug-validate-solver --debug-assignment-validating-solver %t1.bc 2>&1 | FileCheck %s
3+ // RUN: %klee --output-dir=%t.klee-out --search=bfs -- debug-validate-solver --debug-assignment-validating-solver --use-guided-search=none %t1.bc 2>&1 | FileCheck %s
44
55#include "ExerciseSolver.c.inc"
66
7- // CHECK: KLEE: done: completed paths = 9
8- // CHECK: KLEE: done: partially completed paths = 5
7+ // CHECK: KLEE: done: completed paths = 18
8+ // CHECK: KLEE: done: partially completed paths = 0
You can’t perform that action at this time.
0 commit comments