add MC2_function call for assignments where RHS computed from loads; tweak tests

[satcheck.git] / benchmarks / satcheck-precompiled / linuxrwlock / linuxrwlocks.c

diff --git a/benchmarks/satcheck-precompiled/linuxrwlock/linuxrwlocks.c b/benchmarks/satcheck-precompiled/linuxrwlock/linuxrwlocks.c
index 150b68a5b6f83f005eb4823628f398cc4800e44f..a48768b0b2ef1beffe87176035b1376f5814b668 100644 (file)
--- a/benchmarks/satcheck-precompiled/linuxrwlock/linuxrwlocks.c
+++ b/benchmarks/satcheck-precompiled/linuxrwlock/linuxrwlocks.c
@@ -179,8 +179,8 @@ MC2_exitLoop();
 int user_main(int argc, char **argv)
 {
        mylock = (rwlock_t*)malloc(sizeof(rwlock_t));
 int user_main(int argc, char **argv)
 {
        mylock = (rwlock_t*)malloc(sizeof(rwlock_t));

-       _fn1 = MC2_function_id(0, 0, sizeof (mylock), (uint64_t)mylock); 

 
 

+_fn1 = MC2_function_id(0, 0, sizeof (mylock), (uint64_t)mylock); 

        thrd_t t1, t2;
        //, t3, t4;
        MC2_nextOpStoreOffset(_fn1, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP);
        thrd_t t1, t2;
        //, t3, t4;
        MC2_nextOpStoreOffset(_fn1, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP);