diff --git a/src/inputlang/smtlib2/popop_of_smtlib2.ml b/src/inputlang/smtlib2/popop_of_smtlib2.ml index 0763cc47c6bafd3107589745a69ba209f415c1b2..19c69746a626bb397c1be393de9a5dd932cff2a5 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