CIVL=civl
VERIFY=$(CIVL) verify -enablePrintf=false -svcomp

all: bigshot_p_false-unreach-call bigshot_s2_true-unreach-call \
bigshot_s_true-unreach-call fib_bench_false-unreach-call \
fib_bench_longer_false-unreach-call fib_bench_longer_true-unreach-call \
fib_bench_longest_false-unreach-call fib_bench_longest_true-unreach-call \
fib_bench_true-unreach-call indexer_true-unreach-call \
lazy01_false-unreach-call queue_false-unreach-call \
queue_longer_false-unreach-call queue_longest_false-unreach-call \
queue_ok_longer_true-unreach-call queue_ok_longest_true-unreach-call \
queue_ok_true-unreach-call reorder_2_false-unreach-call \
sigma_false-unreach-call singleton_false-unreach-call \
singleton_with-uninit-problems-true stack_false-unreach-call \
stack_longer_false-unreach-call stack_longer_true-unreach-call \
stack_longest_false-unreach-call stack_longest_true-unreach-call \
stack_true-unreach-call stack_true stateful01_false-unreach-call \
stateful01_false stateful01_true-unreach-call stateful01_true \
sync01_true-unreach-call sync01_true twostage_3_false-unreach-call \
twostage_3_false 

bigshot_p_false-unreach-call: bigshot_p_false-unreach-call.c
	$(VERIFY) bigshot_p_false-unreach-call.c

bigshot_s2_true-unreach-call: bigshot_s2_true-unreach-call.c
	$(VERIFY) bigshot_s2_true-unreach-call.c

bigshot_s_true-unreach-call: bigshot_s_true-unreach-call.c
	$(VERIFY) bigshot_s_true-unreach-call.c

fib_bench_false-unreach-call: fib_bench_false-unreach-call.c
	$(VERIFY) -inputNUM=5 fib_bench_false-unreach-call.c

fib_bench_longer_false-unreach-call: fib_bench_longer_false-unreach-call.c
	$(VERIFY) -inputNUM=5 fib_bench_longer_false-unreach-call.c

fib_bench_longer_true-unreach-call: fib_bench_longer_true-unreach-call.c
	$(VERIFY) -inputNUM=5 fib_bench_longer_true-unreach-call.c

fib_bench_longest_false-unreach-call: fib_bench_longest_false-unreach-call.c
	$(VERIFY) -inputNUM=5 fib_bench_longest_false-unreach-call.c

fib_bench_longest_true-unreach-call: fib_bench_longest_true-unreach-call.c
	$(VERIFY) -inputNUM=5 fib_bench_longest_true-unreach-call.c

fib_bench_true-unreach-call: fib_bench_true-unreach-call.c
	$(VERIFY) -inputNUM=5 fib_bench_true-unreach-call.c

indexer_true-unreach-call: indexer_true-unreach-call.c
	$(VERIFY) -inputSIZE=2 -inputMAX=2 -inputNUM_THREADS=2 indexer_true-unreach-call.c

lazy01_false-unreach-call: lazy01_false-unreach-call.c
	$(VERIFY) lazy01_false-unreach-call.c

queue_false-unreach-call: queue_false-unreach-call.c
	$(VERIFY) -inputSIZE=5 -inputEMPTY=-1 -inputFULL=-2 queue_false-unreach-call.c

queue_longer_false-unreach-call: queue_longer_false-unreach-call.c
	$(VERIFY) -inputSIZE=5 -inputEMPTY=-1 -inputFULL=-2 queue_longer_false-unreach-call.c

queue_longest_false-unreach-call: queue_longest_false-unreach-call.c
	$(VERIFY) -inputSIZE=5 -inputEMPTY=-1 -inputFULL=-2 queue_longest_false-unreach-call.c

queue_ok_longer_true-unreach-call: queue_ok_longer_true-unreach-call.c
	$(VERIFY) -inputSIZE=5 -inputEMPTY=-1 -inputFULL=-2 queue_ok_longer_true-unreach-call.c

queue_ok_longest_true-unreach-call: queue_ok_longest_true-unreach-call.c
	$(VERIFY) -inputSIZE=50 -inputEMPTY=-1 -inputFULL=-2 queue_ok_longest_true-unreach-call.c

queue_ok_true-unreach-call: queue_ok_true-unreach-call.c
	$(VERIFY) -inputSIZE=5 -inputEMPTY=-1 -inputFULL=-2 queue_ok_true-unreach-call.c

reorder_2_false-unreach-call: reorder_2_false-unreach-call.c
	$(VERIFY) -inputCIVL_argc=1 reorder_2_false-unreach-call.c

sigma_false-unreach-call: sigma_false-unreach-call.c
	$(VERIFY) sigma_false-unreach-call.c

singleton_false-unreach-call: singleton_false-unreach-call.c
	$(VERIFY) singleton_false-unreach-call.c

singleton_with-uninit-problems-true: singleton_with-uninit-problems-true.c
	$(VERIFY) singleton_with-uninit-problems-true.c

stack_false-unreach-call: stack_false-unreach-call.c
	$(VERIFY) -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_false-unreach-call.c

stack_longer_false-unreach-call: stack_longer_false-unreach-call.c
	$(VERIFY) -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_longer_false-unreach-call.c

stack_longer_true-unreach-call: stack_longer_true-unreach-call.c
	$(VERIFY) -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_longer_true-unreach-call.c

stack_longest_false-unreach-call: stack_longest_false-unreach-call.c
	$(VERIFY) -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_longest_false-unreach-call.c

stack_longest_true-unreach-call: stack_longest_true-unreach-call.c
	$(VERIFY) -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_longest_true-unreach-call.c

stack_true-unreach-call: stack_true-unreach-call.c
	$(VERIFY) -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_true-unreach-call.c

stack_true: stack_true.c
	$(VERIFY) -inputSIZE=5 -inputOVERFLOW=-1 -inputUNDERFLOW=-2 stack_true.c

stateful01_false-unreach-call: stateful01_false-unreach-call.c
	$(VERIFY) stateful01_false-unreach-call.c

stateful01_false: stateful01_false.c
	$(VERIFY) stateful01_false.c

stateful01_true-unreach-call: stateful01_true-unreach-call.c
	$(VERIFY) stateful01_true-unreach-call.c

stateful01_true: stateful01_true.c
	$(VERIFY) stateful01_true.c

sync01_true-unreach-call: sync01_true-unreach-call.c
	$(VERIFY) sync01_true-unreach-call.c

sync01_true: sync01_true.c
	$(VERIFY) sync01_true.c

twostage_3_false-unreach-call: twostage_3_false-unreach-call.c
	$(VERIFY) -inputCIVL_argc=1 twostage_3_false-unreach-call.c

twostage_3_false: twostage_3_false.c
	$(VERIFY) -inputCIVL_argc=1 twostage_3_false.c
