From 14d26164b48a82b86e783ced934fc0399602ce8a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Fri, 8 Jan 2016 14:20:17 +0100
Subject: [PATCH] Updated z3 version, CVC4 and smt-lib format
---
.../leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala | 2 +-
src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala | 2 +-
src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala | 2 +-
src/sphinx/installation.rst | 2 +-
4 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
index 135d47ebc..3a64bd197 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
@@ -15,7 +15,7 @@ class SMTLIBCVC4CounterExampleSolver(context: LeonContext, program: Program) ext
"--rewrite-divk",
"--produce-models",
"--print-success",
- "--lang", "smt",
+ "--lang", "smt2.5",
"--fmf-fun"
) ++ userDefinedOps(ctx)
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index f02cce59c..eaf78aca5 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
@@ -17,7 +17,7 @@ class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTL
Seq(
"-q",
"--print-success",
- "--lang", "smt",
+ "--lang", "smt2.5",
"--quant-ind",
"--rewrite-divk",
"--conjecture-gen",
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
index e2eda5e1c..b71af967f 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -25,7 +25,7 @@ class SMTLIBCVC4Solver(context: LeonContext, program: Program) extends SMTLIBSol
// "--dt-rewrite-error-sel", // Removing since it causes CVC4 to segfault on some inputs
"--rewrite-divk",
"--print-success",
- "--lang", "smt"
+ "--lang", "smt2.5"
) ++ userDefinedOps(ctx).toSeq
}
}
diff --git a/src/sphinx/installation.rst b/src/sphinx/installation.rst
index 1af4a8eaf..b4deaf194 100644
--- a/src/sphinx/installation.rst
+++ b/src/sphinx/installation.rst
@@ -86,7 +86,7 @@ x64, do the following:
2. Copy ``unmanaged/common/vanuatoo*.jar`` to ``unmanaged/64/``
You may be able to obtain additional tips on getting Leon to work on Windows
-from Mikael Mayer, http://people.epfl.ch/mikael.mayer
+from [Mikael Mayer](http://people.epfl.ch/mikael.mayer) or on [his dedicated web page](http://lara.epfl.ch/~mayer/leon/),
.. _smt-solvers:
--
GitLab