Skip to content

Commit cdc1f7f

Browse files
committed
[feat] Prefer a smaller integer vaule in a model
1 parent d0e280b commit cdc1f7f

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

include/klee-test-comp.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,12 +24,14 @@ void __assert_fail(const char *assertion, const char *file, unsigned int line,
2424
int __VERIFIER_nondet_int(void) {
2525
int x;
2626
klee_make_symbolic(&x, sizeof(x), "int");
27+
klee_prefer_cex(&x, x < 1024);
2728
return x;
2829
}
2930

3031
unsigned int __VERIFIER_nondet_uint(void) {
3132
unsigned int x;
3233
klee_make_symbolic(&x, sizeof(x), "unsigned int");
34+
klee_prefer_cex(&x, x < 1024);
3335
return x;
3436
}
3537

0 commit comments

Comments
 (0)