-Q theories iris_c
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files

theories/lib/list.v
theories/lib/mset.v
theories/lib/spin_lock.v
theories/lib/flock.v
theories/lib/locking_heap.v
theories/lib/U.v
theories/c_translation/monad.v
theories/c_translation/proofmode.v
theories/c_translation/translation.v
theories/vcgen/dcexpr.v
theories/vcgen/denv.v
theories/vcgen/splitenv.v
theories/vcgen/vcgen.v
theories/vcgen/vcg_solver.v
theories/tests/basics.v
theories/tests/invoke.v
theories/tests/unknowns.v
theories/tests/swap.v
theories/tests/fact.v
theories/tests/memcpy.v
theories/tests/gcd.v
theories/tests/binop.v
# theories/tests/lists.v