[coreboot-gerrit] Change in libhwbase[master]: Makefile.proof: Reorder theorem provers

[Nico Huber (Code Review)]

Nico Huber has uploaded this change for review. ( https://review.coreboot.org/20627


Change subject: Makefile.proof: Reorder theorem provers
......................................................................

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 at gmx.de>
---
M Makefile.proof
1 file changed, 1 insertion(+), 1 deletion(-)



  git pull ssh://review.coreboot.org:29418/libhwbase refs/changes/27/20627/1

diff --git a/Makefile.proof b/Makefile.proof
index 8b06cdc..45523c3 100644
--- a/Makefile.proof
+++ b/Makefile.proof
@@ -11,7 +11,7 @@
 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)))
 

-- 
To view, visit https://review.coreboot.org/20627
To unsubscribe, visit https://review.coreboot.org/settings

Gerrit-Project: libhwbase
Gerrit-Branch: master
Gerrit-MessageType: newchange
Gerrit-Change-Id: Ia5e1341e881c5f887452486a318e8e72513f28fb
Gerrit-Change-Number: 20627
Gerrit-PatchSet: 1
Gerrit-Owner: Nico Huber <nico.h at gmx.de>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.coreboot.org/pipermail/coreboot-gerrit/attachments/20170717/a0a2d98e/attachment.html>