[klee-dev] KLEE with Non-linear integer constraint; warning about the external 'put'

[Zhoulai]

Hello,

I have two naive questions.

I thought KLEE relies on SMT solver on the theory of linear arithmetics and
therefore, it should be unable to explore path involving non-linear
relation.  But I am surprised by the results from testing a program with a
simple polynomial constraint:








*#include <klee/klee.h>#include <stdio.h>int foo(int x) {  int y =
x*x*x+x*x+x;  if (y == 1110){     .......  }*

*  return 0;*







*} int main() {  int a;  klee_make_symbolic(&a, sizeof(a), "a");  return
foo(a);} *
KLEE successfully triggers the branch 'y==1110', Why?

*Another question:* I got a warning from symbolically executing the program
above:

*KLEE: WARNING ONCE: calling external: puts(169520648)*

What does the warning mean?

Thanks for your ideas.
Zhoulai
-------------- next part --------------
HTML attachment scrubbed and removed