Gabriele

False positive "Read-write" data race with barrier-protected global memory access

2

I am running the following (minimal) example ``` int sread(__global unsigned int *L) { barrier(CLK_GLOBAL_MEM_FENCE); int r = *L; barrier(CLK_GLOBAL_MEM_FENCE); return r; } __kernel void manager(__global unsigned int *L) {...

When adding (declare-const Name Type) to SmtLibScript and dumping the script on file, the output contains `(declare-const Name () Type)` The extra parentheses () seem to violate the SMT syntax....