Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Pzucker/precondition #101

Merged
merged 3 commits into from
Dec 5, 2019
Merged

Pzucker/precondition #101

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
70dd0f4
Initial commit of precondition smtlib code
philzook58 Nov 21, 2019
01e18a7
Made suggested changes. Added tests. Make a z3_utils file
philzook58 Dec 5, 2019
2d64676
updated desciprtion on z3_utils.mli
philzook58 Dec 5, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions wp/lib/bap_wp/src/compare.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,19 +130,19 @@ let mk_smtlib2_compare (env1 : Env.t) (env2 : Env.t) (smtlib_str : string) : Con
String.substr_replace_all smtlib_str ~pattern:((Var.name var) ^ "_mod") ~with_:(Z3.Expr.to_string z3_var)
) in
info "New smtlib string: %s \n" smtlib_str;
let declsym1 = Env.get_decls_and_symbols env1 in
let declsym2 = Env.get_decls_and_symbols env2 in
let declsym1 = Z3_utils.get_decls_and_symbols env1 in
let declsym2 = Z3_utils.get_decls_and_symbols env2 in
let declsym = declsym1 @ declsym2 in
let ctx = Env.get_context env1 in
Constr.mk_smtlib2 ctx smtlib_str declsym
Z3_utils.mk_smtlib2 ctx smtlib_str declsym

let compare_subs_eq
~input:(input : Var.Set.t)
~output:(output : Var.Set.t)
~original:(original : Sub.t * Env.t)
~modified:(modified : Sub.t * Env.t)
~smtlib_post:(smtlib_post : string)
~smtlib_pre:(smtlib_pre : string)
~smtlib_hyp:(smtlib_hyp : string)
: Constr.t * Env.t * Env.t =
let postcond ~original:(_, env1) ~modified:(_, env2) ~rename_set:_ =
let post_eqs, env1, env2 = set_to_eqs env1 env2 output in
Expand All @@ -151,7 +151,7 @@ let compare_subs_eq
in
let hyps ~original:(_, env1) ~modified:(_, env2) ~rename_set:_ =
let pre_eqs, env1, env2 = set_to_eqs env1 env2 input in
let pre' = mk_smtlib2_compare env1 env2 smtlib_pre in
let pre' = mk_smtlib2_compare env1 env2 smtlib_hyp in
Constr.mk_clause [] (pre' :: pre_eqs), env1, env2
in
compare_subs ~postcond:postcond ~hyps:hyps ~original:original ~modified:modified
Expand Down
2 changes: 1 addition & 1 deletion wp/lib/bap_wp/src/compare.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ val compare_subs_eq
-> original:(Bap.Std.Sub.t * Env.t)
-> modified:(Bap.Std.Sub.t * Env.t)
-> smtlib_post:string
-> smtlib_pre:string
-> smtlib_hyp:string
-> Constr.t * Env.t * Env.t

(** Compare two subroutines by composition for an empty postcondition:
Expand Down
19 changes: 0 additions & 19 deletions wp/lib/bap_wp/src/constraint.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -271,22 +271,3 @@ let get_refuted_goals ?filter_out:(filter_out = []) (constr : t)
worker constr Jmp.Map.empty Jmp.Map.empty [] []


let mk_smtlib2 (ctx : Z3.context) (smtlib_str : string) (decl_syms : (Z3.FuncDecl.func_decl * Z3.Symbol.symbol) list) : t =
let fun_decls, fun_symbols = List.unzip decl_syms in
let sort_symbols = [] in
let sorts = [] in
let asts = Z3.SMT.parse_smtlib2_string ctx smtlib_str
sort_symbols
sorts
fun_symbols
fun_decls
in
let goals = List.map (Z3.AST.ASTVector.to_expr_list asts)
~f:(fun e ->
e
|> mk_goal (Expr.to_string e)
|> mk_constr)
in
mk_clause [] goals


7 changes: 1 addition & 6 deletions wp/lib/bap_wp/src/constraint.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -127,9 +127,4 @@ val eval_model_exn : Z3.Model.model -> z3_expr -> z3_expr
(** Gets the model of the last check to the Z3 solver. An error will be raised
if retrieving the model fails in the case that [check] was not yet called
to the solver or the result of the last [check] did not result in SAT. *)
val get_model_exn : Z3.Solver.solver -> Z3.Model.model

(** [mk_smtlib2] parses a string in the context that already has a mapping of func_decl to symbols
and returns a constraint [Constr.t] *)

val mk_smtlib2 : Z3.context -> string -> ((Z3.FuncDecl.func_decl * Z3.Symbol.symbol) list) -> t
val get_model_exn : Z3.Solver.solver -> Z3.Model.model
6 changes: 3 additions & 3 deletions wp/lib/bap_wp/src/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
(library
(name bap_wp)
(public_name bap_wp)
(libraries bap bap-x86-cpu z3 oUnit))
(name bap_wp)
(public_name bap_wp)
(libraries bap bap-x86-cpu z3 oUnit))
27 changes: 3 additions & 24 deletions wp/lib/bap_wp/src/environment.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -274,6 +274,9 @@ let get_subs (env : t) : Sub.t Seq.t =
let get_var_map (env : t) : Constr.z3_expr EnvMap.t =
env.var_map

let find_var (env : t) (var : Var.t) : Constr.z3_expr option =
EnvMap.find env.var_map var

let get_var (env : t) (var : Var.t) : Constr.z3_expr * t =
let mv = EnvMap.find env.var_map var in
match mv with
Expand Down Expand Up @@ -331,27 +334,3 @@ let is_x86 (a : Arch.t) : bool =

let use_input_regs (env : t) : bool =
env.fun_input_regs

let get_decls_and_symbols (env : t) : ((Z3.FuncDecl.func_decl * Z3.Symbol.symbol) list) =
let var_map = get_var_map env in
let ctx = get_context env in
EnvMap.fold var_map ~init:[]
~f:(fun ~key:_ ~data:z3_var decls ->
assert (Z3.Expr.is_const z3_var);
let decl = Z3.FuncDecl.mk_const_decl_s ctx
(Z3.Expr.to_string z3_var)
(Z3.Expr.get_sort z3_var) in
let sym = Z3.Symbol.mk_string ctx (Z3.Expr.to_string z3_var) in
(decl,sym)::decls
)

let mk_smtlib2_single (env : t) (smt_post : string) : Constr.t =
let var_map = get_var_map env in
let smt_post = EnvMap.fold var_map ~init:smt_post
~f:(fun ~key:var ~data:z3_var smt_post ->
String.substr_replace_all smt_post ~pattern:((Var.name var) ^ " ") ~with_:((Z3.Expr.to_string z3_var) ^ " ")
) in
info "New smt-lib string : %s\n" smt_post;
let decl_syms = get_decls_and_symbols env in
let ctx = get_context env in
Constr.mk_smtlib2 ctx smt_post decl_syms
21 changes: 4 additions & 17 deletions wp/lib/bap_wp/src/environment.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,9 @@ val add_var : t -> Bap.Std.Var.t -> Constr.z3_expr -> t
(** Remove a binding in the environment for a bap variable. *)
val remove_var : t -> Bap.Std.Var.t -> t

(** Looks up the Z3 variable that represents a BIR variable. *)
val find_var : t -> Bap.Std.Var.t -> Constr.z3_expr option

(** Add a precondition to be associated to a block b to the environment. *)
val add_precond : t -> Bap.Std.Tid.t -> Constr.t -> t

Expand All @@ -149,7 +152,7 @@ val get_subs : t -> Bap.Std.Sub.t Bap.Std.Seq.t
(** Obtains the var_map containing a mapping of BIR variables to Z3 variables. *)
val get_var_map : t -> Constr.z3_expr EnvMap.t

(** Looks up the Z3 variable that represents a BIR variable. *)
(** Looks up the Z3 variable that represents a BIR variable. Produces fresh z3_expr if not found. *)
val get_var : t -> Bap.Std.Var.t -> Constr.z3_expr * t

(** Looks up the precondition for a given block in the environment. Currently returns
Expand Down Expand Up @@ -212,20 +215,4 @@ val mk_z3_expr : Z3.context -> name:string -> typ:Bap.Std.Type.t -> Constr.z3_ex
constant is "fresh" with the {!Environment.var_gen}. *)
val new_z3_expr : ?name:string -> t -> Bap.Std.Type.t -> Constr.z3_expr


(** [get_decls_and_symbols] builds from a the var_map in an environment
a mapping of all Z3 func_decl to their symbol. This is a helper function for
[mk_smtlib2] *)

val get_decls_and_symbols : t -> ((Z3.FuncDecl.func_decl * Z3.Symbol.symbol) list)


(** [mk_smtlib2_single env smtlib_str] takes in a string representing a
valid SMT-Lib-2 statement.
The variables in the SMT-Lib statements need to appear in the
environment. The intended purpose of this function is generating hypothesis
and postconditions for single binary analysis *)
val mk_smtlib2_single : t -> string -> Constr.t


(*---------------------------------------------------*)
6 changes: 5 additions & 1 deletion wp/lib/bap_wp/src/precondition.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -217,9 +217,13 @@ let exp_to_z3 (exp : Exp.t) (env : Env.t) : Constr.z3_expr * Constr.t list * Con
debug "Visiting let %s = %s in %s%!"
(Var.to_string v) (Exp.to_string exp) (Exp.to_string body);
let exp_val, env = exp_to_z3_body exp env in
let old_val = Env.find_var env v in
let env' = Env.add_var env v exp_val in
let z3_expr, env = exp_to_z3_body body env' in
let env = Env.remove_var env v in
let env = match old_val with
| None -> env
| Some exp_val -> Env.add_var env v exp_val in
(z3_expr, env)
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If a variable in the let-binding shares a name with a variable that already existed in the env, would removing it also remove the original variable? If so, it might be good to write a comment about that.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Correct, this could conceivable occur if some pervert wanted to name a let-bound variable RAX, or more pragmatically if an inner let shadows an outer let. This should cause a run-time error rather than a mysterious change in semantics. A comment might be appropriate though.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm. That's an interesting point. We didn't implement this correctly basically. We should store the variable we're covering up. In practice it probably isn't a problem because the let bindings seem to use names like "$1", but should probably still be fixed for sanity

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a really good catch

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think I fixed this

| Unknown (str, typ) ->
debug "Visiting unknown: %s Type:%s%!" str (Type.to_string typ);
Expand Down Expand Up @@ -858,7 +862,7 @@ let check ?refute:(refute = true) (solver : Solver.solver) (ctx : Z3.context)
else
pre'
in
Printf.printf "Z3 Query:\n%s\n" (Z3.Expr.to_string (Z3.Expr.simplify is_correct None));
info "Z3 Query:\n%s\n" (Z3.Expr.to_string (Z3.Expr.simplify is_correct None));
let () = Z3.Solver.add solver [is_correct] in
Z3.Solver.check solver []

Expand Down
71 changes: 71 additions & 0 deletions wp/lib/bap_wp/src/z3_utils.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
(***************************************************************************)
(* *)
(* Copyright (C) 2018/2019 The Charles Stark Draper Laboratory, Inc. *)
(* *)
(* This file is provided under the license found in the LICENSE file in *)
(* the top-level directory of this project. *)
(* *)
(* This work is funded in part by ONR/NAWC Contract N6833518C0107. Its *)
(* content does not necessarily reflect the position or policy of the US *)
(* Government and no official endorsement should be inferred. *)
(* *)
(***************************************************************************)

open !Core_kernel
open Bap.Std

include Self()

module Expr = Z3.Expr
module Arith = Z3.Arithmetic
module BV = Z3.BitVector
module Bool = Z3.Boolean
module Z3Array = Z3.Z3Array
module FuncDecl = Z3.FuncDecl
module Symbol = Z3.Symbol
module Solver = Z3.Solver
module Env = Environment
module Constr = Constraint

let get_decls_and_symbols (env : Env.t) : ((FuncDecl.func_decl * Symbol.symbol) list) =
let var_map = Env.get_var_map env in
let ctx = Env.get_context env in
Env.EnvMap.fold var_map ~init:[]
~f:(fun ~key:_ ~data:z3_var decls ->
assert (Expr.is_const z3_var);
let decl = FuncDecl.mk_const_decl_s ctx
(Expr.to_string z3_var)
(Expr.get_sort z3_var) in
let sym = Symbol.mk_string ctx (Expr.to_string z3_var) in
(decl,sym)::decls
)

let mk_smtlib2 (ctx : Z3.context) (smtlib_str : string) (decl_syms : (Z3.FuncDecl.func_decl * Z3.Symbol.symbol) list) : Constr.t =
let fun_decls, fun_symbols = List.unzip decl_syms in
let sort_symbols = [] in
let sorts = [] in
let asts = Z3.SMT.parse_smtlib2_string ctx smtlib_str
sort_symbols
sorts
fun_symbols
fun_decls
in
let goals = List.map (Z3.AST.ASTVector.to_expr_list asts)
~f:(fun e ->
e
|> Constr.mk_goal (Expr.to_string e)
|> Constr.mk_constr)
in
Constr.mk_clause [] goals

let mk_smtlib2_single (env : Env.t) (smt_post : string) : Constr.t =
let var_map = Env.get_var_map env in
let smt_post = Env.EnvMap.fold var_map ~init:smt_post
~f:(fun ~key:var ~data:z3_var smt_post ->
String.substr_replace_all smt_post ~pattern:((Var.name var) ^ " ") ~with_:((Expr.to_string z3_var) ^ " ")
) in
info "New smt-lib string : %s\n" smt_post;
let decl_syms = get_decls_and_symbols env in
let ctx = Env.get_context env in
mk_smtlib2 ctx smt_post decl_syms

47 changes: 47 additions & 0 deletions wp/lib/bap_wp/src/z3_utils.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
(***************************************************************************)
(* *)
(* Copyright (C) 2018/2019 The Charles Stark Draper Laboratory, Inc. *)
(* *)
(* This file is provided under the license found in the LICENSE file in *)
(* the top-level directory of this project. *)
(* *)
(* This work is funded in part by ONR/NAWC Contract N6833518C0107. Its *)
(* content does not necessarily reflect the position or policy of the US *)
(* Government and no official endorsement should be inferred. *)
(* *)
(***************************************************************************)

(**

This module exports types and utilities to process and report results found
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can we update this comment to match the z3_utils module?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed. Good catch.

using the WP plugin.

The report contains information about the result of the WP analysis, and in
the case the result is [SAT], prints out the model that contains the input
register and memory values that result in the program refuting a goal, the path
taken to the refuted goal, and the register values at each jump in the path.

*)

module Env = Environment
module Constr = Constraint


(** [get_decls_and_symbols] builds from a the var_map in an environment
a mapping of all Z3 func_decl to their symbol. This is a helper function for
[mk_smtlib2] *)
val get_decls_and_symbols : Env.t -> ((Z3.FuncDecl.func_decl * Z3.Symbol.symbol) list)

(** [mk_smtlib2_single env smtlib_str] takes in a string representing a
valid SMT-Lib-2 statement.
The variables in the SMT-Lib statements need to appear in the
environment. The intended purpose of this function is generating hypothesis
and postconditions for single binary analysis *)
val mk_smtlib2_single : Env.t -> string -> Constr.t

(** [mk_smtlib2] parses a smtlib2 string in the context that has a mapping of func_decl
to symbols and returns a constraint [Constr.t] corresponding to the smtlib2 string.
The [func_decl * symbol] mapping can be constructed from an [Env.t] using the
[get_decls_and_symbols] function. *)

val mk_smtlib2 : Z3.context -> string -> ((Z3.FuncDecl.func_decl * Z3.Symbol.symbol) list) -> Constr.t
22 changes: 12 additions & 10 deletions wp/lib/bap_wp/tests/unit/test_compare.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,7 @@ let test_sub_pair_1 (test_ctx : test_ctxt) : unit =
let output_vars = Var.Set.singleton z in
let compare_prop, _, _ = Comp.compare_subs_eq
~input:input_vars ~output:output_vars
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_pre:"" in
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_hyp:"" in
assert_z3_compare test_ctx ~orig:env1 ~modif:env2
(Sub.to_string sub1) (Sub.to_string sub2)
compare_prop Z3.Solver.UNSATISFIABLE
Expand Down Expand Up @@ -163,7 +163,7 @@ let test_sub_pair_2 (test_ctx : test_ctxt) : unit =
let output_vars = Var.Set.singleton z in
let compare_prop, _, _ = Comp.compare_subs_eq
~input:input_vars ~output:output_vars
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_pre:"" in
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_hyp:"" in
assert_z3_compare test_ctx ~orig:env1 ~modif:env2
(Sub.to_string sub1) (Sub.to_string sub2)
compare_prop Z3.Solver.SATISFIABLE
Expand Down Expand Up @@ -197,7 +197,7 @@ let test_sub_pair_3 (test_ctx : test_ctxt) : unit =
let output_vars = Var.Set.singleton z in
let compare_prop, _, _ = Comp.compare_subs_eq
~input:input_vars ~output:output_vars
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_pre:"" in
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_hyp:"" in
assert_z3_compare test_ctx ~orig:env1 ~modif:env2
(Sub.to_string sub1) (Sub.to_string sub2)
compare_prop Z3.Solver.UNSATISFIABLE
Expand Down Expand Up @@ -234,7 +234,7 @@ let test_sub_pair_4 (test_ctx : test_ctxt) : unit =
let output_vars = Var.Set.singleton y in
let compare_prop, _, _ = Comp.compare_subs_eq
~input:input_vars ~output:output_vars
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_pre:"" in
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_hyp:"" in
assert_z3_compare test_ctx ~orig:env1 ~modif:env2
(Sub.to_string sub1) (Sub.to_string sub2)
compare_prop Z3.Solver.UNSATISFIABLE
Expand Down Expand Up @@ -271,7 +271,7 @@ let test_sub_pair_5 (test_ctx : test_ctxt) : unit =
let output_vars = Var.Set.singleton y in
let compare_prop, _, _ = Comp.compare_subs_eq
~input:input_vars ~output:output_vars
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_pre:"" in
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_hyp:"" in
assert_z3_compare test_ctx ~orig:env1 ~modif:env2
(Sub.to_string sub1) (Sub.to_string sub2)
compare_prop Z3.Solver.SATISFIABLE
Expand Down Expand Up @@ -462,7 +462,7 @@ let test_fun_outputs_1 (test_ctx : test_ctxt) : unit =
let output_vars = Var.Set.singleton ret_var in
let compare_prop, _, _ = Comp.compare_subs_eq
~input:input_vars ~output:output_vars
~original:(main_sub1, env1) ~modified:(main_sub2, env2) ~smtlib_post:"" ~smtlib_pre:"" in
~original:(main_sub1, env1) ~modified:(main_sub2, env2) ~smtlib_post:"" ~smtlib_hyp:"" in
assert_z3_compare test_ctx ~orig:env1 ~modif:env2
(Sub.to_string main_sub1)
(Sub.to_string main_sub2)
Expand Down Expand Up @@ -495,7 +495,7 @@ let test_fun_outputs_2 (test_ctx : test_ctxt) : unit =
let output_vars = Var.Set.singleton ret_var in
let compare_prop, _, _ = Comp.compare_subs_eq
~input:input_vars ~output:output_vars
~original:(main_sub1, env1) ~modified:(main_sub2, env2) ~smtlib_post:"" ~smtlib_pre:"" in
~original:(main_sub1, env1) ~modified:(main_sub2, env2) ~smtlib_post:"" ~smtlib_hyp:"" in
assert_z3_compare test_ctx ~orig:env1 ~modif:env2
(Sub.to_string main_sub1)
(Sub.to_string main_sub2)
Expand Down Expand Up @@ -533,7 +533,8 @@ let test_fun_outputs_3 (test_ctx : test_ctxt) : unit =
let output_vars = Var.Set.singleton rax in
let compare_prop, _, _ = Comp.compare_subs_eq
~input:input_vars ~output:output_vars
~original:(main_sub1, env1) ~modified:(main_sub2, env2) in
~original:(main_sub1, env1) ~modified:(main_sub2, env2)
~smtlib_post:"" ~smtlib_hyp:"" in
assert_z3_compare test_ctx ~orig:env1 ~modif:env2
(Sub.to_string main_sub1)
(Sub.to_string main_sub2)
Expand Down Expand Up @@ -571,7 +572,8 @@ let test_fun_outputs_4 (test_ctx : test_ctxt) : unit =
let output_vars = Var.Set.singleton rax in
let compare_prop, _, _ = Comp.compare_subs_eq
~input:input_vars ~output:output_vars
~original:(main_sub1, env1) ~modified:(main_sub2, env2) in
~original:(main_sub1, env1) ~modified:(main_sub2, env2)
~smtlib_post:"" ~smtlib_hyp:"" in
assert_z3_compare test_ctx ~orig:env1 ~modif:env2
(Sub.to_string main_sub1)
(Sub.to_string main_sub2)
Expand Down Expand Up @@ -599,7 +601,7 @@ let test_sub_pair_mem_1 (test_ctx : test_ctxt) : unit =
let output_vars = Var.Set.singleton mem in
let compare_prop, _, _ = Comp.compare_subs_eq
~input:input_vars ~output:output_vars
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_pre:"" in
~original:(sub1,env1) ~modified:(sub2,env2) ~smtlib_post:"" ~smtlib_hyp:"" in
assert_z3_compare test_ctx ~orig:env1 ~modif:env2
(Sub.to_string sub1) (Sub.to_string sub2)
compare_prop Z3.Solver.SATISFIABLE
Expand Down
Loading