mirror of
https://github.com/Telecominfraproject/OpenCellular.git
synced 2026-01-17 18:41:22 +00:00
Makefile.proof: Reorder theorem provers
Prefer Z3 over CVC4, the latter seems to not do anything for the current code and just wastes CPU cycles. Change-Id: Ia5e1341e881c5f887452486a318e8e72513f28fb Signed-off-by: Nico Huber <nico.h@gmx.de> Reviewed-on: https://review.coreboot.org/20627 Reviewed-by: Paul Menzel <paulepanter@users.sourceforge.net> Reviewed-by: Adrian-Ken Rueegsegger <ken@codelabs.ch>
This commit is contained in:
@@ -11,7 +11,7 @@ SPARKFLAGS += -m
|
||||
SPARKFLAGS += --mode=$(PROOF_MODE)
|
||||
SPARKFLAGS += --report=fail
|
||||
SPARKFLAGS += --warnings=error
|
||||
SPARKFLAGS += --prover=cvc4,z3 --steps=500 --timeout=1 # FIXME: timeout used because steps seems broken
|
||||
SPARKFLAGS += --prover=z3,cvc4 --steps=500 --timeout=1 # FIXME: timeout used because steps seems broken
|
||||
|
||||
quote-list = $(subst $(space),$(comma),$(patsubst %,"%",$(1)))
|
||||
|
||||
|
||||
Reference in New Issue
Block a user