From 33170d1d7eaa4c9609d41472a5fb0de9e7e76a6b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Sun, 29 Dec 2013 17:05:21 +0100
Subject: [PATCH] [SMT2] add QF_UFLRA
---
src/inputlang/smtlib2/popop_of_smtlib2.ml | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/src/inputlang/smtlib2/popop_of_smtlib2.ml b/src/inputlang/smtlib2/popop_of_smtlib2.ml
index 0763cc47c..19c69746a 100644
--- a/src/inputlang/smtlib2/popop_of_smtlib2.ml
+++ b/src/inputlang/smtlib2/popop_of_smtlib2.ml
@@ -177,6 +177,11 @@ let of_decl sched benv = function
let env = Scheduler.Scheduler.get_delayed sched in
Arith.propagate env;
DStr.H.add benv.ctr "Real" Arith.real_ctr
+ | CSetLogic (_,Symbol(_,"QF_UFLRA")) ->
+ let env = Scheduler.Scheduler.get_delayed sched in
+ Uninterp.propagate env;
+ Arith.propagate env;
+ DStr.H.add benv.ctr "Real" Arith.real_ctr
| CSetLogic (loc,_) -> raise (Not_supported loc)
| CDeclareSort(_,Symbol(_,name),arity) ->
declare_sort benv name arity
--
GitLab