diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala index 135d47ebcb1bb0a492d46258b81e840d0916c75f..3a64bd19737e9f7c7f15c78c0044a71f49721df8 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 f02cce59c78a4e81b3071248b747127fdce4797d..eaf78aca5e78cb49fe1ccf3bb7d07556514c61d0 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 e2eda5e1cc84da7e72fcea0f4b1ce24ff6d91fc9..b71af967f9671fd13f7c6a4625e592649fb470ba 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 1af4a8eaffb032fce8d512e25556a9ffaae3fb72..b4deaf194eb4f84eac0b14dabb42221cfb999056 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: