diff options
| author | Alasdair Armstrong | 2019-12-06 16:08:08 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-12-06 16:42:51 +0000 |
| commit | d66f510ba6ab9e453c8410fb7a1cab570dd17236 (patch) | |
| tree | 6c6b5e7b940da44fa508ff62a035e6f6c02724d2 /src/jib/jib_smt.ml | |
| parent | 4d3c99561eed6016d5f85502ab188be6a80a27c2 (diff) | |
Don't introduce uneccesary control flow when compiling
Diffstat (limited to 'src/jib/jib_smt.ml')
| -rw-r--r-- | src/jib/jib_smt.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 725d2a89..8a700dbd 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -346,8 +346,6 @@ let rec smt_cval ctx cval = Fn ("not", [Fn ("=", [smt_cval ctx cval1; smt_cval ctx cval2])]) | V_call (Bvor, [cval1; cval2]) -> Fn ("bvor", [smt_cval ctx cval1; smt_cval ctx cval2]) - | V_call (Bit_to_bool, [cval]) -> - Fn ("=", [smt_cval ctx cval; Bitvec_lit [Sail2_values.B1]]) | V_call (Eq, [cval1; cval2]) -> Fn ("=", [smt_cval ctx cval1; smt_cval ctx cval2]) | V_call (Bnot, [cval]) -> |