@@ -22,9 +22,9 @@ def klee_options(
2222 write_ktests ,
2323):
2424 if max_time and int (max_time ) > 30 :
25- MAX_SOLVER_TIME = 10
25+ MAX_SOLVER_TIME = 15
2626 else :
27- MAX_SOLVER_TIME = 5
27+ MAX_SOLVER_TIME = 10
2828 cmd = [
2929 "--strip-unwanted-calls" , # removes llvm.dbg.* instructions, exponentially reduces time on some benchmarks
3030 "--delete-dead-loops=false" , # without this optimizer removes some code, which decreases coverage
@@ -33,10 +33,11 @@ def klee_options(
3333 "--external-calls=all" ,
3434 "--use-forked-solver=false" ,
3535 # "--solver-backend=stp",
36- "--solver-backend=z3-tree" ,
36+ # "--solver-backend=z3-tree",
37+ "--solver-backend=bitwuzla-tree" ,
3738 "--max-solvers-approx-tree-inc=16" ,
3839 f"--max-memory={ int (max_memory * 0.9 )} " , # Just use half of the memory in case we have to fork
39- "--optimize " ,
40+ "--libc=klee " ,
4041 "--skip-not-lazy-initialized" ,
4142 f"--output-dir={ test_output_dir } " , # Output files into specific directory
4243 "--output-source=false" , # Do not output assembly.ll - it can be too large
@@ -53,7 +54,6 @@ def klee_options(
5354 # "--libc=uclibc",
5455 # "--posix-runtime",
5556 "--fp-runtime" ,
56- "--x86FP-as-x87FP80=false" ,
5757 # "--max-sym-array-size=4096",
5858 "--symbolic-allocation-threshold=8192" ,
5959 "--uninit-memory-test-multiplier=10" ,
@@ -68,19 +68,21 @@ def klee_options(
6868 "--allocate-determ" ,
6969 f"--allocate-determ-size={ min (int (max_memory * 0.6 ), 3 * 1024 )} " ,
7070 "--allocate-determ-start-address=0x00030000000" ,
71+ "--x86FP-as-x87FP80" ,
7172 ]
7273
7374 if f_err :
7475 cmd += [
75- "--use-alpha-equivalence=false" ,
76+ "--optimize=true" ,
77+ "--use-alpha-equivalence=true" ,
7678 "--function-call-reproduce=reach_error" ,
77- "--dump-states-on-halt-with-function-call-reproduce" ,
7879 # "--max-cycles=0",
7980 # "--tc-type=bug",
8081 "--dump-states-on-halt=unreached" , # Explicitly do not dump states
8182 "--exit-on-error-type=Assert" , # Only generate test cases of type assert
8283 # "--dump-test-case-type=Assert", # Only dump test cases of type assert
8384 "--search=dfs" ,
85+ "--search=bfs" ,
8486 # "--search=nurs:covnew", "--search=random-path","--search=dfs", "--use-batching-search",
8587 # "--search=distance","--search=random-path","--use-batching-search",
8688 # "--target-assert", # Target
@@ -97,8 +99,10 @@ def klee_options(
9799
98100 if f_cov :
99101 cmd += [
102+ "--optimize=false" ,
100103 "--mem-trigger-cof" , # Start on the fly tests generation after approaching memory cup
101104 "--use-alpha-equivalence=true" ,
105+ "--optimize-aggressive=false" ,
102106 "--track-coverage=all" , # Only branches and only instructions are wrong in real life. E.g., ternary operators are sometimes counted as different branches, while we stick to look at them as a single instruction from a single branch
103107 "--use-iterative-deepening-search=max-cycles" ,
104108 f"--max-solver-time={ MAX_SOLVER_TIME } s" ,
@@ -273,6 +277,7 @@ class KLEEF(object):
273277
274278 def run (self ):
275279 test_output_dir = self .test_results_path / self .source .name
280+ test_output_dir = self .test_results_path
276281 # Clean-up from previous runs if needed
277282 shutil .rmtree (test_output_dir , ignore_errors = True )
278283
0 commit comments