Commit aacb881c authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

fix meta "select_lskept" "all"

parent 85275b96
......@@ -4,7 +4,7 @@ prelude ";;; this is a prelude for MathSAT5"
prelude "(set-logic AUFNIRA)"
printer "smtv2"
filename "%f-%t-%g.smt"
filename "%f-%t-%g.smt2"
valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" ""
......
......@@ -4,7 +4,7 @@ prelude ";;; this is a prelude for Z3"
prelude "(set-logic AUFNIRA)"
printer "smtv2"
filename "%f-%t-%g.smt"
filename "%f-%t-%g.smt2"
valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" ""
......
......@@ -65,6 +65,8 @@ module Lskept = struct
let add_lskept sls ls = if good_for_inst ls then Sls.add ls sls else sls
let all_lskept task sls = match task.task_decl.td_node with
| Decl { d_node = Dparam ls } ->
add_lskept sls ls
| Decl { d_node = Dlogic l } ->
List.fold_left (fun sls (ls,_) -> add_lskept sls ls) sls l
| _ -> sls
......
Markdown is supported
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