Set logic to QF_AUFLIRA for Yices-smt2, as it will not even start parsing the input file otherwise.

109ba0d4 · Guillaume Melquiond · 8d4cf301 · 109ba0d4
Commit 109ba0d4 authored Aug 25, 2017 by Guillaume Melquiond
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

drivers/yices-smt2.drv drivers/yices-smt2.drv +1 -1

No files found.
--- a/drivers/yices-smt2.drv
+++ b/drivers/yices-smt2.drv
 (* Why3 driver for Yices-smt2 solver *)

 prelude ";;; this is a prelude for Yices-smt2"
-prelude "(set-logic AUFLIRA)"
+prelude "(set-logic QF_AUFLIRA)"
 (* A  : Array
   UF : Uninterpreted Function
   LIRA : Linear Integer Reals Arithmetic