From 85e73bfaf51c25e2a630556b0465e1c341b6713d Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 15 Apr 2015 16:41:32 +0200
Subject: [PATCH] Mention smt-cvc4 in help as a viable solver
---
src/main/scala/leon/Main.scala | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index c1da63048..f130f363e 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -37,7 +37,7 @@ object Main {
LeonFlagOptionDef ("synthesis", "--synthesis", "Partial synthesis of choose() constructs"),
LeonFlagOptionDef ("xlang", "--xlang", "Support for extra program constructs (imperative,...)"),
LeonFlagOptionDef ("watch", "--watch", "Rerun pipeline when file changes"),
- LeonValueOptionDef("solvers", "--solvers=s1,s2", "Use solvers s1 and s2 (fairz3,enum,smt)"),
+ LeonValueOptionDef("solvers", "--solvers=s1,s2", "Use solvers s1 and s2 (fairz3,enum,smt-z3,smt-cvc4)"),
LeonValueOptionDef("debug", "--debug=<sections..>", "Enables specific messages"),
LeonFlagOptionDef ("noop", "--noop", "No operation performed, just output program"),
LeonFlagOptionDef ("help", "--help", "Show help")
--
GitLab