From cdc1f7ff8c2ff13d13177eace57f502130f09c07 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Tue, 17 Oct 2023 00:08:54 +0400 Subject: [PATCH] [feat] Prefer a smaller integer vaule in a model --- include/klee-test-comp.c | 2 ++ 1 file changed, 2 insertions(+) diff --git a/include/klee-test-comp.c b/include/klee-test-comp.c index bad3b783d0..90774aa2b2 100644 --- a/include/klee-test-comp.c +++ b/include/klee-test-comp.c @@ -24,12 +24,14 @@ void __assert_fail(const char *assertion, const char *file, unsigned int line, int __VERIFIER_nondet_int(void) { int x; klee_make_symbolic(&x, sizeof(x), "int"); + klee_prefer_cex(&x, x < 1024); return x; } unsigned int __VERIFIER_nondet_uint(void) { unsigned int x; klee_make_symbolic(&x, sizeof(x), "unsigned int"); + klee_prefer_cex(&x, x < 1024); return x; }