Actions
Bug #507
openSMT sovler could not parse the request (Error: Undefined name)
Status:
New
Priority:
Low
Assignee:
-
Category:
-
Target version:
-
Start date:
10/27/2010
Due date:
% Done:
0%
Estimated time:
Detected in build:
ebfe9ed48e0684365a6f8aacb0b8c22e82157b8a
Platform:
Linux x86
Published in build:
Description
Blast fails with exception
ZZZ: Exception: Failure("SMT sovler answer is strange: Error: Undefined name \"-1073741824\".")
on the attached driver.
Command line:
LDV_DEBUG=100 BLAST_EXP_NOALIAS=1 RCV_TIMELIMIT=900 RCV_MEMLIMIT=1800000 BLAST_SOLVER=yices BLAST_OPTIONS="-devdebug" ldv-manager tag=current envs=linux-2.6.31.6.tar.bz2 drivers=wl12xx.ko.tar.bz2 "rule_models=32_7"
If comment the following line in spi.c then the result will be unsafe.
void wl12xx_spi_read(struct wl12xx *wl, int addr, void *buf,
size_t len)
...
//cmd |= WSPI_CMD_READ;
Files
Actions