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

[satcheck.git] / benchmarks / satcheck-precompiled / linuxlock / linuxlocks.c

diff --git a/benchmarks/satcheck-precompiled/linuxlock/linuxlocks.c b/benchmarks/satcheck-precompiled/linuxlock/linuxlocks.c
index db7502555ac3c663b07b881dbb1ac619511147de..366a1639b5406a4ba5bfd040ee0a6497f23c1903 100644 (file)
--- a/benchmarks/satcheck-precompiled/linuxlock/linuxlocks.c
+++ b/benchmarks/satcheck-precompiled/linuxlock/linuxlocks.c
@@ -58,8 +58,8 @@ int user_main(int argc, char **argv)
 {
        thrd_t t1, t2;//, t3, t4;
        mylock = (rwlock_t*)malloc(sizeof(rwlock_t));
-       _fn0 = MC2_function_id(0, 0, sizeof (mylock), (uint64_t)mylock); 
-       MC2_nextOpStoreOffset(_fn0, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP);
+
+       _fn0 = MC2_function_id(0, 0, sizeof (mylock), (uint64_t)mylock);        MC2_nextOpStoreOffset(_fn0, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP);
        store_32(&mylock->lock, 0);
 
        thrd_create(&t1, (thrd_start_t)&a, NULL);