Skip to content
Snippets Groups Projects
Commit 33170d1d authored by François Bobot's avatar François Bobot
Browse files

[SMT2] add QF_UFLRA

parent f3396d89
No related branches found
No related tags found
No related merge requests found
...@@ -177,6 +177,11 @@ let of_decl sched benv = function ...@@ -177,6 +177,11 @@ let of_decl sched benv = function
let env = Scheduler.Scheduler.get_delayed sched in let env = Scheduler.Scheduler.get_delayed sched in
Arith.propagate env; Arith.propagate env;
DStr.H.add benv.ctr "Real" Arith.real_ctr 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) | CSetLogic (loc,_) -> raise (Not_supported loc)
| CDeclareSort(_,Symbol(_,name),arity) -> | CDeclareSort(_,Symbol(_,name),arity) ->
declare_sort benv name arity declare_sort benv name arity
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment