Hi,
I am trying to use a previous version of klee on "seq".
I am running with these parameters:
klee --simplify-sym-indices --max-sym-array-size 4096 --write-cvcs --
write-cov --output-module --max-memory=3000 --disable-inlining --use-
forked-stp --use-cex-cache --with-libc --with-file-model=release --
allow-external-sym-calls --exclude-libc-cov --optimize --only-output-
states-covering-new --run-in=/home/zamf/sandbox --max-instruction-
time=10. --max-time=3600. --watchdog --max-memory-inhibit=false --max-
static-fork-pct=1 --max-static-solve-pct=1 --max-static-cpfork-pct=1 --
switch-type=internal --randomize-fork --use-random-path --use-
interleaved-covnew-NURS --use-batching-search --batch-instructions
10000 --init-env ./seq.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-
files 1 8 --sym-stdout
and I get this error
DEMAND FAILED:util/FloatEvaluation.h:ext:193: <inWidth==32> is false:
"can only extend from a 32-bit float"
The error comes from the first demand in this function which is called
with inWidth = 64.
// extension of l (which must be a float) to double (casts a float to
a double)
inline uint64_t ext(uint64_t l, unsigned outWidth, unsigned inWidth) {
klee_warning("inwidth = %d", inWidth);
demand( inWidth==32, "can only extend from a 32-bit float" );
demand( outWidth==64, "can only extend to a 64-bit double" );
double ext = (double)UInt64AsFloat(l);
return bits64::truncateToNBits(DoubleAsUInt64(ext), outWidth);
}
from lib/util/FloatEvaluation.h
Did you run into this error before?
Thank you,
Cristi
