From 0118c3579b59637180aa049753294674bcfd5619 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 10 Jun 2015 19:59:53 +0200
Subject: [PATCH] Include GroundSolver in docs
---
doc/options.rst | 4 ++++
src/main/scala/leon/solvers/SolverFactory.scala | 2 +-
2 files changed, 5 insertions(+), 1 deletion(-)
diff --git a/doc/options.rst b/doc/options.rst
index 96dfcb94f..368526aee 100644
--- a/doc/options.rst
+++ b/doc/options.rst
@@ -161,6 +161,10 @@ These options are available by all Leon components:
* ``unrollz3``
Native Z3, but inductive reasoning happens within Leon (similarly to ``smt-z3``).
+
+ * ``ground``
+
+ Only solves ground verification conditions (without variables) by evaluating them.
* ``--strict``
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 42479fa01..64cf6e3d7 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -37,7 +37,7 @@ object SolverFactory {
"smt-cvc4-proof" -> "CVC4 through SMT-LIB, in-solver inductive reasoning, for proofs only",
"smt-cvc4-cex" -> "CVC4 through SMT-LIB, in-solver finite-model-finding, for counter-examples only",
"unrollz3" -> "Native Z3 with leon-templates for unfolding",
- "ground" -> "Only solves ground terms by evaluating them",
+ "ground" -> "Only solves ground verification conditions by evaluating them",
"enum" -> "Enumeration-based counter-example-finder"
)
--
GitLab