Commit 952c0ae2 authored by Aymeric Varasse's avatar Aymeric Varasse
Browse files

Fixed pp_header to allow "QF_LRA" to be printed

parent cc6ae076
......@@ -43,7 +43,8 @@ let rec stringify = function
(* Header of the SMTLIB2 file *)
let pp_header t =
let logic_str = match t with
| Linear_Real_Theory | Real_Theory -> "QF_NRA"
| Linear_Real_Theory -> "QF_LRA"
| Real_Theory -> "QF_NRA"
| Float_Theory -> "QF_FP"
in
[";;This file has been generated with onnx2SMTtool";
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment