[klee-dev] klee_assert hangs (1 symbolic integer)

[Wei Ming Khoo]

Hi devs,

I ran the following on klee-cde-v1 and klee-cde-v2 with the same outcome.

#include<klee/klee.h>
int p1(int x){
  int x1=x;
  return x1*x1+2*x+1;
}

int p2(int x){
  int x1=x;
  return x1*x+2*x+1;
}

int p3(int x){
  return x*x+2*x+1;
}

int p4(int x){
  return (x+1)*(x+1);
}

int main(){
  int x;
  klee_make_symbolic( &x, sizeof(x), "x" );
  // This passes without failed assertions
  //klee_assert( p3(x) == p4(x) );
  // This passes without failed assertions
  //klee_assert( p2(x) == p4(x) );
  // This hangs
  klee_assert( p1(x) == p4(x) );
  return 0;
}

The first 2 tests passed, but the third hung (I killed it after 30 mins).
I ran with -debug-print-instructions and it hangs on the klee_assert statement.
I ran with -use-stp-query-pc-log but the stp-queries.qlog file was empty.

Any idea what went wrong? Or what else I could try doing?

Regards,
--wm
_______________________________________________
klee-dev mailing list
klee-dev@keeda.stanford.edu
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev