From c3dcbab6c458d502bc04f80a9362667cadfab789 Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Mon, 16 May 2022 01:11:10 +0200
Subject: [PATCH 1/6] augment gitignore

---
 .gitignore | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.gitignore b/.gitignore
index 19664536..cbb78213 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,4 @@
-# Generated by Cargo
-# will have compiled files and executables
 /target/
-/src/common/revision.rs
\ No newline at end of file
+/src/common/revision.rs
+.vscode
+.DS_Store
\ No newline at end of file

From c4e50e2c34d5ca3a504a3000c527da735cac99b7 Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Mon, 16 May 2022 01:11:29 +0200
Subject: [PATCH 2/6] fix warnings

---
 src/common/macros.rs | 4 ++--
 src/term/eval.rs     | 4 ++--
 src/val.rs           | 1 -
 3 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/common/macros.rs b/src/common/macros.rs
index d9ef5943..f8fa9e2b 100644
--- a/src/common/macros.rs
+++ b/src/common/macros.rs
@@ -356,10 +356,10 @@ macro_rules! msg {
     }
   ) ;
   ( force $slf:expr => $e:tt ) => (
-    $slf.msg($e) ? ;
+    $slf.msg($e) ?
   ) ;
   ( force $slf:expr => $($tt:tt)* ) => (
-    $slf.msg( format!( $($tt)* ) ) ? ;
+    $slf.msg( format!( $($tt)* ) ) ?
   ) ;
   ( $core:expr => $e:expr ) => (
     if_debug!( $core.msg($e) ? )
diff --git a/src/term/eval.rs b/src/term/eval.rs
index a49d8509..16d8deaa 100644
--- a/src/term/eval.rs
+++ b/src/term/eval.rs
@@ -37,10 +37,10 @@ pub fn eval<E: Evaluator>(term: &Term, model: &E) -> Res<Val> {
 
 macro_rules! go {
     (up $e:expr) => {
-        return Ok(ZipDo::Upp { yielded: $e });
+        return Ok(ZipDo::Upp { yielded: $e })
     };
     (down $e:expr) => {
-        return Ok(ZipDo::Dwn { nu_term: $e });
+        return Ok(ZipDo::Dwn { nu_term: $e })
     };
 }
 
diff --git a/src/val.rs b/src/val.rs
index bb65c060..8001d179 100644
--- a/src/val.rs
+++ b/src/val.rs
@@ -896,7 +896,6 @@ impl RVal {
     /// assert!{ res.is_err() }
     /// ```
     pub fn g_t(&self, other: &Val) -> Res<Val> {
-        #[allow(unused_parens)]
         arith_bin_rel! { * self, gt, * other.get() }
     }
 

From 10697109af542c82514dbbe07f369dd5ab460a8e Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Mon, 16 May 2022 01:51:36 +0200
Subject: [PATCH 3/6] updated most deps, fixed tests, bumped z3 to 4.8.17

---
 .github/workflows/ci.yml |   6 +-
 Cargo.lock               | 205 ++++++++++++++++++++++-----------------
 Cargo.toml               |   4 +-
 src/common.rs            |  38 ++++----
 src/common/config.rs     | 116 +++++++++++-----------
 src/common/msg.rs        |  12 +--
 src/data.rs              |  22 ++---
 7 files changed, 217 insertions(+), 186 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index c146248d..a9cf5ea7 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -16,11 +16,9 @@ jobs:
         ]
         include:
         - os: macos-latest
-          Z3_DOWNLOAD: "https://github.com/Z3Prover/z3/releases/download/z3-4.8.7/z3-4.8.7-x64-osx-10.14.6.zip"
-        # - os: windows-latest
-        #   Z3_DOWNLOAD: "https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/ z3-4.8.10-x64-win.zip"
+          Z3_DOWNLOAD: "https://github.com/Z3Prover/z3/releases/download/z3-4.8.17/z3-4.8.17-x64-osx-10.16.zip"
         - os: ubuntu-latest
-          Z3_DOWNLOAD: "https://github.com/Z3Prover/z3/releases/download/z3-4.8.7/z3-4.8.7-x64-ubuntu-16.04.zip"
+          Z3_DOWNLOAD: "https://github.com/Z3Prover/z3/releases/download/z3-4.8.17/z3-4.8.17-x64-glibc-2.31.zip"
 
     runs-on: ${{ matrix.os }}
 
diff --git a/Cargo.lock b/Cargo.lock
index a20ed3b6..d774db5d 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1,10 +1,12 @@
 # This file is automatically @generated by Cargo.
 # It is not intended for manual editing.
+version = 3
+
 [[package]]
 name = "addr2line"
-version = "0.14.1"
+version = "0.17.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a55f82cfe485775d02112886f4169bde0c5894d75e79ead7eafe7e40a25e45f7"
+checksum = "b9ecd88a8c8378ca913a680cd98f0f13ac67383d35993f86c90a70e3f137816b"
 dependencies = [
  "gimli",
 ]
@@ -15,15 +17,6 @@ version = "1.0.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f26201604c87b1e01bd3d98f8d5d9a8fcbb815e8cedb41ffccbeb4bf593a35fe"
 
-[[package]]
-name = "ansi_term"
-version = "0.11.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ee49baf6cb617b853aa8d93bf420db2383fab46d314482ca2803b40d5fde979b"
-dependencies = [
- "winapi",
-]
-
 [[package]]
 name = "ansi_term"
 version = "0.12.1"
@@ -46,17 +39,18 @@ dependencies = [
 
 [[package]]
 name = "autocfg"
-version = "1.0.1"
+version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cdb031dd78e28731d87d56cc8ffef4a8f36ca26c38fe2de700543e627f8a464a"
+checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa"
 
 [[package]]
 name = "backtrace"
-version = "0.3.56"
+version = "0.3.65"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9d117600f438b1707d4e4ae15d3595657288f8235a0eb593e80ecc98ab34e1bc"
+checksum = "11a17d453482a265fd5f8479f2a3f405566e6ca627837aaddb85af8b1ab8ef61"
 dependencies = [
  "addr2line",
+ "cc",
  "cfg-if",
  "libc",
  "miniz_oxide",
@@ -66,9 +60,15 @@ dependencies = [
 
 [[package]]
 name = "bitflags"
-version = "1.2.1"
+version = "1.3.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cf1de2fe8c75bc145a2f577add951f8134889b4795d47466a54a5c846d691693"
+checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
+
+[[package]]
+name = "cc"
+version = "1.0.73"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2fff2a6927b3bb87f9595d67196a70493f627687a71d87a0d692242c33f58c11"
 
 [[package]]
 name = "cfg-if"
@@ -78,17 +78,27 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
 [[package]]
 name = "clap"
-version = "2.33.3"
+version = "3.1.18"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "37e58ac78573c40708d45522f0d80fa2f01cc4f9b4e2bf749807255454312002"
+checksum = "d2dbdf4bdacb33466e854ce889eee8dfd5729abf7ccd7664d0a2d60cd384440b"
 dependencies = [
- "ansi_term 0.11.0",
  "atty",
  "bitflags",
+ "clap_lex",
+ "indexmap",
+ "lazy_static",
  "strsim",
+ "termcolor",
  "textwrap",
- "unicode-width",
- "vec_map",
+]
+
+[[package]]
+name = "clap_lex"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a37c35f1112dad5e6e0b1adaff798507497a18fceeb30cceb3bae7d1427b9213"
+dependencies = [
+ "os_str_bytes",
 ]
 
 [[package]]
@@ -109,9 +119,9 @@ dependencies = [
 
 [[package]]
 name = "getrandom"
-version = "0.2.2"
+version = "0.2.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c9495705279e7140bf035dde1f6e750c162df8b625267cd52cc44e0b156732c8"
+checksum = "9be70c98951c83b8d2f8f60d7065fa6d5146873094452a1008da8c2f1e4205ad"
 dependencies = [
  "cfg-if",
  "libc",
@@ -120,24 +130,28 @@ dependencies = [
 
 [[package]]
 name = "gimli"
-version = "0.23.0"
+version = "0.26.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f6503fe142514ca4799d4c26297c4248239fe8838d827db6bd6065c6ed29a6ce"
+checksum = "78cc372d058dcf6d5ecd98510e7fbc9e5aec4d21de70f65fea8fecebcd881bd4"
 
 [[package]]
-name = "hashconsing"
-version = "1.3.0"
+name = "hashbrown"
+version = "0.11.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ec4594a62a29e1a867076005a660671a1121de786435b76acad955a59cb72075"
+checksum = "ab5ef0d4909ef3724cc8cce6ccc8572c5c817592e9285f5464f8e86f8bd3726e"
+
+[[package]]
+name = "hashconsing"
+version = "1.5.0"
 dependencies = [
  "lazy_static",
 ]
 
 [[package]]
 name = "hermit-abi"
-version = "0.1.18"
+version = "0.1.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "322f4de77956e22ed0e5032c359a0f1273f1f7f0d79bfa3b8ffbc730d7fbcc5c"
+checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33"
 dependencies = [
  "libc",
 ]
@@ -146,7 +160,7 @@ dependencies = [
 name = "hoice"
 version = "1.9.0"
 dependencies = [
- "ansi_term 0.12.1",
+ "ansi_term",
  "atty",
  "clap",
  "either",
@@ -161,6 +175,16 @@ dependencies = [
  "rsmt2",
 ]
 
+[[package]]
+name = "indexmap"
+version = "1.8.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0f647032dfaa1f8b6dc29bd3edb7bbef4861b8b8007ebb118d6db284fd59f6ee"
+dependencies = [
+ "autocfg",
+ "hashbrown",
+]
+
 [[package]]
 name = "lazy_static"
 version = "1.4.0"
@@ -169,18 +193,23 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
 
 [[package]]
 name = "libc"
-version = "0.2.93"
+version = "0.2.125"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5916d2ae698f6de9bfb891ad7a8d65c09d232dc58cc4ac433c7da3b2fd84bc2b"
+
+[[package]]
+name = "memchr"
+version = "2.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9385f66bf6105b241aa65a61cb923ef20efc665cb9f9bb50ac2f0c4b7f378d41"
+checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d"
 
 [[package]]
 name = "miniz_oxide"
-version = "0.4.4"
+version = "0.5.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a92518e98c078586bc6c934028adcca4c92a53d6a958196de835170a01d84e4b"
+checksum = "d2b29bd4bc3f33391105ebee3589c19197c4271e3e5a9ec9bfe8127eeff8f082"
 dependencies = [
  "adler",
- "autocfg",
 ]
 
 [[package]]
@@ -188,7 +217,7 @@ name = "mylib"
 version = "0.1.0"
 source = "git+https://github.com/AdrienChampion/mylib#62fecec97b9d8f9088731badcf5e1963e46af43d"
 dependencies = [
- "ansi_term 0.12.1",
+ "ansi_term",
 ]
 
 [[package]]
@@ -207,9 +236,9 @@ dependencies = [
 
 [[package]]
 name = "num-bigint"
-version = "0.4.0"
+version = "0.4.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4e0d047c1062aa51e256408c560894e5251f08925980e53cf1aa5bd00eec6512"
+checksum = "f93ab6289c7b344a8a9f60f88d80aa20032336fe78da341afc91c8a2341fc75f"
 dependencies = [
  "autocfg",
  "num-integer",
@@ -218,18 +247,18 @@ dependencies = [
 
 [[package]]
 name = "num-complex"
-version = "0.4.0"
+version = "0.4.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "26873667bbbb7c5182d4a37c1add32cdf09f841af72da53318fdb81543c15085"
+checksum = "97fbc387afefefd5e9e39493299f3069e14a140dd34dc19b4c1c1a8fddb6a790"
 dependencies = [
  "num-traits",
 ]
 
 [[package]]
 name = "num-integer"
-version = "0.1.44"
+version = "0.1.45"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d2cc698a63b549a70bc047073d2949cce27cd1c7b0a4a862d08a8031bc2801db"
+checksum = "225d3389fb3509a24c93f5c29eb6bde2586b98d9f016636dff58d7c6f7569cd9"
 dependencies = [
  "autocfg",
  "num-traits",
@@ -237,9 +266,9 @@ dependencies = [
 
 [[package]]
 name = "num-iter"
-version = "0.1.42"
+version = "0.1.43"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b2021c8337a54d21aca0d59a92577a029af9431cb59b909b03252b9c164fad59"
+checksum = "7d03e6c028c5dc5cac6e2dec0efda81fc887605bb3d884578bb6d6bf7514e252"
 dependencies = [
  "autocfg",
  "num-integer",
@@ -260,42 +289,50 @@ dependencies = [
 
 [[package]]
 name = "num-traits"
-version = "0.2.14"
+version = "0.2.15"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9a64b1ec5cda2586e284722486d802acf1f7dbdc623e2bfc57e65ca1cd099290"
+checksum = "578ede34cf02f8924ab9447f50c28075b4d3e5b269972345e7e0372b38c6cdcd"
 dependencies = [
  "autocfg",
 ]
 
 [[package]]
 name = "object"
-version = "0.23.0"
+version = "0.28.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a9a7ab5d64814df0fe4a4b5ead45ed6c5f181ee3ff04ba344313a6c80446c5d4"
+checksum = "e42c982f2d955fac81dd7e1d0e1426a7d702acd9c98d19ab01083a6a0328c424"
+dependencies = [
+ "memchr",
+]
+
+[[package]]
+name = "os_str_bytes"
+version = "6.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "029d8d0b2f198229de29dca79676f2738ff952edf3fde542eb8bf94d8c21b435"
 
 [[package]]
 name = "ppv-lite86"
-version = "0.2.10"
+version = "0.2.16"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ac74c624d6b2d21f425f752262f42188365d7b8ff1aff74c82e45136510a4857"
+checksum = "eb9f9e6e233e5c4a35559a617bf40a4ec447db2e84c20b55a6f83167b7e57872"
 
 [[package]]
 name = "rand"
-version = "0.8.3"
+version = "0.8.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0ef9e7e66b4468674bfcb0c81af8b7fa0bb154fa9f28eb840da5c447baeb8d7e"
+checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404"
 dependencies = [
  "libc",
  "rand_chacha",
  "rand_core",
- "rand_hc",
 ]
 
 [[package]]
 name = "rand_chacha"
-version = "0.3.0"
+version = "0.3.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e12735cf05c9e10bf21534da50a147b924d555dc7a547c42e6bb2d5b6017ae0d"
+checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88"
 dependencies = [
  "ppv-lite86",
  "rand_core",
@@ -303,22 +340,13 @@ dependencies = [
 
 [[package]]
 name = "rand_core"
-version = "0.6.2"
+version = "0.6.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "34cf66eb183df1c5876e2dcf6b13d57340741e8dc255b48e40a26de954d06ae7"
+checksum = "d34f1408f55294453790c48b2f1ebbb1c5b4b7563eb1f418bcfcfdbb06ebb4e7"
 dependencies = [
  "getrandom",
 ]
 
-[[package]]
-name = "rand_hc"
-version = "0.3.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3190ef7066a446f2e7f42e239d161e905420ccab01eb967c9eb27d21b2322a73"
-dependencies = [
- "rand_core",
-]
-
 [[package]]
 name = "rand_xorshift"
 version = "0.3.0"
@@ -339,42 +367,36 @@ dependencies = [
 
 [[package]]
 name = "rustc-demangle"
-version = "0.1.18"
+version = "0.1.21"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6e3bad0ee36814ca07d7968269dd4b7ec89ec2da10c4bb613928d3077083c232"
+checksum = "7ef03e0a2b150c7a90d01faf6254c9c48a41e95fb2a8c2ac1c6f0d2b9aefc342"
 
 [[package]]
 name = "strsim"
-version = "0.8.0"
+version = "0.10.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a"
+checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623"
 
 [[package]]
-name = "textwrap"
-version = "0.11.0"
+name = "termcolor"
+version = "1.1.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d326610f408c7a4eb6f51c37c330e496b08506c9457c9d34287ecc38809fb060"
+checksum = "bab24d30b911b2376f3a13cc2cd443142f0c81dda04c118693e35b3835757755"
 dependencies = [
- "unicode-width",
+ "winapi-util",
 ]
 
 [[package]]
-name = "unicode-width"
-version = "0.1.8"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9337591893a19b88d8d87f2cec1e73fad5cdfd10e5a6f349f498ad6ea2ffb1e3"
-
-[[package]]
-name = "vec_map"
-version = "0.8.2"
+name = "textwrap"
+version = "0.15.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f1bddf1187be692e79c5ffeab891132dfb0f236ed36a43c7ed39f1165ee20191"
+checksum = "b1141d4d61095b28419e22cb0bbf02755f5e54e0526f97f1e3d1d160e60885fb"
 
 [[package]]
 name = "version_check"
-version = "0.9.3"
+version = "0.9.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5fecdca9a5291cc2b8dcf7dc02453fee791a280f3743cb0905f8822ae463b3fe"
+checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f"
 
 [[package]]
 name = "wasi"
@@ -398,6 +420,15 @@ version = "0.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
 
+[[package]]
+name = "winapi-util"
+version = "0.1.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "70ec6ce85bb158151cae5e5c87f95a8e97d2c0c4b001223f33a334e3ce5de178"
+dependencies = [
+ "winapi",
+]
+
 [[package]]
 name = "winapi-x86_64-pc-windows-gnu"
 version = "0.4.0"
diff --git a/Cargo.toml b/Cargo.toml
index db5b1cfc..d12e8814 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -34,8 +34,8 @@ bench = [ ]
 [dependencies]
 libc = "*"
 lazy_static = "*"
-clap = "*"
-hashconsing = "*"
+clap = { version = "*", features = ["cargo"] }
+hashconsing = { path = "../hashconsing" }
 error-chain = "*"
 ansi_term = "*"
 rsmt2 = "^0.12"
diff --git a/src/common.rs b/src/common.rs
index ddee76e1..71175efc 100644
--- a/src/common.rs
+++ b/src/common.rs
@@ -1,10 +1,11 @@
 //! Base types and functions.
 
 use clap::crate_version;
-use mylib::impl_fmt;
 
 pub use std::{
     collections::{BTreeMap, BTreeSet},
+    collections::{HashMap, HashSet},
+    fmt,
     io::stdout,
     io::{
         Result as IoRes, {Read, Write},
@@ -17,9 +18,8 @@ pub use std::{
 
 pub use either::Either;
 pub use error_chain::bail;
-pub use hashconsing::{coll::*, HashConsed, HashConsign};
+pub use hashconsing::{hash_coll::*, HashConsed, HashConsign};
 pub use lazy_static::lazy_static;
-pub use mylib::common::hash::*;
 pub use num::{One, Signed, Zero};
 pub use rand_xorshift::XorShiftRng as Rng;
 pub use rsmt2::{actlit::Actlit, print::Expr2Smt, SmtRes, Solver};
@@ -331,15 +331,15 @@ impl Bias {
         }
     }
 }
-impl_fmt! {
-  Bias(self, fmt) {
-    match * self {
-      Bias::Lft => write!(fmt, "left"),
-      Bias::Rgt => write!(fmt, "right"),
-      Bias::NuRgt(pred, ref args) => write!(fmt, "right({} {})", pred, args),
-      Bias::Non => write!(fmt, "none"),
+impl fmt::Display for Bias {
+    fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
+        match *self {
+            Bias::Lft => write!(fmt, "left"),
+            Bias::Rgt => write!(fmt, "right"),
+            Bias::NuRgt(pred, ref args) => write!(fmt, "right({} {})", pred, args),
+            Bias::Non => write!(fmt, "none"),
+        }
     }
-  }
 }
 
 /// Alias type for a counterexample for a clause.
@@ -543,14 +543,16 @@ impl std::ops::AddAssign for RedInfo {
         self.args_rmed += args_rmed
     }
 }
-impl_fmt! {
-  RedInfo(self, fmt) {
-    write!(
-      fmt, "\
+impl fmt::Display for RedInfo {
+    fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
+        write!(
+            fmt,
+            "\
         prd: {}, cls rm: {}, cls add: {}, args rm: {}\
-      ", self.preds, self.clauses_rmed, self.clauses_added, self.args_rmed
-    )
-  }
+      ",
+            self.preds, self.clauses_rmed, self.clauses_added, self.args_rmed
+        )
+    }
 }
 
 // |===| Helper traits.
diff --git a/src/common/config.rs b/src/common/config.rs
index 5d783ce1..411e7236 100644
--- a/src/common/config.rs
+++ b/src/common/config.rs
@@ -25,7 +25,7 @@ macro_rules! app_fun {
         $id:ident($($stuff:tt)*) $($tail:tt)*
     ) => ({
         let arg = app_fun!(
-            @arg Arg::with_name(stringify!($id)).display_order(*$order) => $($stuff)*
+            @arg Arg::new(stringify!($id)).display_order(*$order) => $($stuff)*
         );
         *$order += 1;
         let app = $app.arg(arg);
@@ -59,8 +59,8 @@ macro_rules! app_fun {
     (@arg $arg:expr => val_nb $val_nb:expr, $($stuff:tt)*) => (
         app_fun!(@arg $arg.number_of_values($val_nb) => $($stuff)*)
     );
-    (@arg $arg:expr => hidden, $($stuff:tt)*) => (
-        app_fun!(@arg $arg.hidden(true) => $($stuff)*)
+    (@arg $arg:expr => hide, $($stuff:tt)*) => (
+        app_fun!(@arg $arg.hide(true) => $($stuff)*)
     );
     (@arg $arg:expr => $(,)*) => ($arg);
     (@arg $arg:expr => $stuff:tt) => (
@@ -137,9 +137,9 @@ macro_rules! make_conf {
 }
 
 /// Clap `App` with static lifetimes.
-pub type App = ::clap::App<'static, 'static>;
+pub type App = ::clap::Command<'static>;
 /// Clap `ArgMatches` with static lifetime.
-pub type Matches = ::clap::ArgMatches<'static>;
+pub type Matches = ::clap::ArgMatches;
 
 /// Functions all sub-configurations must have.
 pub trait SubConf {
@@ -352,7 +352,7 @@ make_conf! {
             val_nb 1,
             validator bool_validator,
             default "on",
-            hidden,
+            hide,
         } {
             |val| bool_of_match(val)
         }
@@ -385,7 +385,7 @@ make_conf! {
             val_nb 1,
             validator bool_validator,
             default "no",
-            hidden,
+            hide,
         } {
             |val| bool_of_match(val)
         }
@@ -403,7 +403,7 @@ make_conf! {
             val_nb 1,
             validator bool_validator,
             default "on",
-            hidden,
+            hide,
         } {
             |val| bool_of_match(val)
         }
@@ -421,7 +421,7 @@ make_conf! {
             val_nb 1,
             validator bool_validator,
             default "on",
-            hidden,
+            hide,
         } {
             |val| bool_of_match(val)
         }
@@ -439,7 +439,7 @@ make_conf! {
             val_nb 1,
             validator bool_validator,
             default "on",
-            hidden,
+            hide,
         } {
             |val| bool_of_match(val)
         }
@@ -457,7 +457,7 @@ make_conf! {
             val_nb 1,
             validator bool_validator,
             default "on",
-            hidden,
+            hide,
         } {
             |val| bool_of_match(val)
         }
@@ -491,7 +491,7 @@ make_conf! {
             val_nb 1,
             validator bool_validator,
             default "off",
-            hidden,
+            hide,
         } {
             |val| bool_of_match(val)
         }
@@ -509,7 +509,7 @@ make_conf! {
             val_nb 1,
             validator bool_validator,
             default "on",
-            hidden,
+            hide,
         } {
             |val| bool_of_match(val)
         }
@@ -527,7 +527,7 @@ make_conf! {
             val_nb 1,
             validator bool_validator,
             default "on",
-            hidden,
+            hide,
         } {
             |val| bool_of_match(val)
         }
@@ -580,7 +580,7 @@ make_conf! {
             val_nb 1,
             validator bool_validator,
             default "on",
-            hidden,
+            hide,
         } {
             |val| bool_of_match(val)
         }
@@ -597,7 +597,7 @@ make_conf! {
             val_nb 1,
             validator bool_validator,
             default "on",
-            hidden,
+            hide,
         } {
             |val| bool_of_match(val)
         }
@@ -723,7 +723,7 @@ make_conf! {
             default "40",
             takes_val,
             val_nb 1,
-            hidden,
+            hide,
         } {
             |mtch| {
                 let value = int_of_match(mtch) as f64 / 100.;
@@ -750,7 +750,7 @@ make_conf! {
             default "on",
             takes_val,
             val_nb 1,
-            hidden,
+            hide,
         } {
             |mtch| bool_of_match(mtch)
         }
@@ -821,7 +821,7 @@ make_conf! {
             default "10",
             takes_val,
             val_nb 1,
-            hidden,
+            hide,
         } {
             |mtch| {
                 let value = int_of_match(mtch) as f64 / 100.0;
@@ -847,7 +847,7 @@ make_conf! {
             default "10",
             takes_val,
             val_nb 1,
-            hidden,
+            hide,
         } {
             |mtch| {
                 let value = int_of_match(mtch) as f64 / 100.0;
@@ -873,7 +873,7 @@ make_conf! {
             default "0",
             takes_val,
             val_nb 1,
-            hidden,
+            hide,
         } {
             |mtch| {
                 let value = int_of_match(mtch) as f64 / 100.0;
@@ -899,7 +899,7 @@ make_conf! {
                 default "100000",
                 takes_val,
                 val_nb 1,
-                hidden,
+                hide,
         } {
             |mtch| int_of_match(mtch)
         }
@@ -917,7 +917,7 @@ make_conf! {
             default "no",
             takes_val,
             val_nb 1,
-            hidden,
+            hide,
         } {
             |mtch| bool_of_match(mtch)
         }
@@ -934,7 +934,7 @@ make_conf! {
             default "on",
             takes_val,
             val_nb 1,
-            hidden,
+            hide,
         } {
             |mtch| bool_of_match(mtch)
         }
@@ -951,7 +951,7 @@ make_conf! {
             default "on",
             takes_val,
             val_nb 1,
-            hidden,
+            hide,
         } {
             |mtch| bool_of_match(mtch)
         }
@@ -968,7 +968,7 @@ make_conf! {
             default "off",
             takes_val,
             val_nb 1,
-            hidden,
+            hide,
         } {
             |mtch| bool_of_match(mtch)
         }
@@ -985,7 +985,7 @@ make_conf! {
             default "off",
             takes_val,
             val_nb 1,
-            hidden,
+            hide,
         } {
             |mtch| bool_of_match(mtch)
         }
@@ -1063,7 +1063,7 @@ make_conf! {
             default "off",
             takes_val,
             val_nb 1,
-            hidden,
+            hide,
         } {
             |mtch| bool_of_match(mtch)
         }
@@ -1097,7 +1097,7 @@ make_conf! {
             default "off",
             takes_val,
             val_nb 1,
-            hidden,
+            hide,
         } {
             |mtch| bool_of_match(mtch)
         }
@@ -1306,31 +1306,31 @@ impl Config {
             .version(*crate::common::version)
             .about("ICE engine for systems described as Horn Clauses.")
             .arg(
-                Arg::with_name("input file")
+                Arg::new("input file")
                     .help("sets the input file to use")
                     .index(1)
                     .display_order(order()),
             )
             .arg(
-                Arg::with_name("verb")
-                    .short("-v")
+                Arg::new("verb")
+                    .short('v')
                     .help("increases verbosity")
                     .takes_value(false)
-                    .multiple(true)
+                    .multiple_occurrences(true)
                     .display_order(order()),
             )
             .arg(
-                Arg::with_name("quiet")
-                    .short("-q")
+                Arg::new("quiet")
+                    .short('q')
                     .help("decreases verbosity")
                     .takes_value(false)
-                    .multiple(true)
+                    .multiple_occurrences(true)
                     .display_order(order()),
             )
             .arg(
-                Arg::with_name("color")
+                Arg::new("color")
                     .long("--color")
-                    .short("-c")
+                    .short('c')
                     .help("(de)activates coloring (off if output is not a tty)")
                     .validator(bool_validator)
                     .value_name(bool_format)
@@ -1340,9 +1340,9 @@ impl Config {
                     .display_order(order()),
             )
             .arg(
-                Arg::with_name("out_dir")
+                Arg::new("out_dir")
                     .long("--out_dir")
-                    .short("-o")
+                    .short('o')
                     .help("sets the output directory")
                     .value_name("DIR")
                     .default_value("hoice_out")
@@ -1351,9 +1351,9 @@ impl Config {
                     .display_order(order()),
             )
             .arg(
-                Arg::with_name("stats")
+                Arg::new("stats")
                     .long("--stats")
-                    .short("-s")
+                    .short('s')
                     .help("reports some statistics at the end of the run")
                     .validator(bool_validator)
                     .value_name(bool_format)
@@ -1363,9 +1363,9 @@ impl Config {
                     .display_order(order()),
             )
             .arg(
-                Arg::with_name("infer")
+                Arg::new("infer")
                     .long("--infer")
-                    .short("-i")
+                    .short('i')
                     .help("if `off`, ignore `check-sat` and `get-model` queries")
                     .validator(bool_validator)
                     .value_name(bool_format)
@@ -1375,9 +1375,9 @@ impl Config {
                     .display_order(order()),
             )
             .arg(
-                Arg::with_name("timeout")
+                Arg::new("timeout")
                     .long("--timeout")
-                    .short("-t")
+                    .short('t')
                     .help("sets a timeout in seconds, `0` for none")
                     .validator(int_validator)
                     .value_name("int")
@@ -1387,7 +1387,7 @@ impl Config {
                     .display_order(order()),
             )
             .arg(
-                Arg::with_name("split")
+                Arg::new("split")
                     .long("--split")
                     .help("reason on each negative clause separately")
                     .validator(bool_validator)
@@ -1398,7 +1398,7 @@ impl Config {
                     .display_order(order()),
             )
             .arg(
-                Arg::with_name("split_step")
+                Arg::new("split_step")
                     .long("--split_step")
                     .help("pause between negative clauses in split mode")
                     .validator(bool_validator)
@@ -1409,7 +1409,7 @@ impl Config {
                     .display_order(order()),
             )
             .arg(
-                Arg::with_name("term_simpl")
+                Arg::new("term_simpl")
                     .long("--term_simpl")
                     .help("level of term simplification between 0 and 3")
                     .validator(int_validator)
@@ -1418,10 +1418,10 @@ impl Config {
                     .takes_value(true)
                     .number_of_values(1)
                     .display_order(order())
-                    .hidden(true),
+                    .hide(true),
             )
             .arg(
-                Arg::with_name("check_simpl")
+                Arg::new("check_simpl")
                     .long("--check_simpl")
                     .help("if true, check all simplifications")
                     .validator(bool_validator)
@@ -1430,7 +1430,7 @@ impl Config {
                     .takes_value(true)
                     .number_of_values(1)
                     .display_order(order())
-                    .hidden(true),
+                    .hide(true),
             )
     }
 
@@ -1442,7 +1442,7 @@ impl Config {
         };
 
         app.arg(
-            Arg::with_name("check")
+            Arg::new("check")
                 .long("--check")
                 .help("checks a model for the input system (does not run inference)")
                 .value_name("FILE")
@@ -1451,7 +1451,7 @@ impl Config {
                 .display_order(order()),
         )
         .arg(
-            Arg::with_name("check_eld")
+            Arg::new("check_eld")
                 .long("--check_eld")
                 .help("if `check` is active, expect eldarica-style result")
                 .validator(bool_validator)
@@ -1588,9 +1588,9 @@ pub fn int_of_matches(matches: &Matches, key: &str) -> usize {
 
 /// Validates integer input.
 #[cfg_attr(feature = "cargo-clippy", allow(needless_pass_by_value))]
-pub fn int_validator(s: String) -> Result<(), String> {
+pub fn int_validator(s: &str) -> Result<(), String> {
     use std::str::FromStr;
-    match usize::from_str(&s) {
+    match usize::from_str(s) {
         Ok(_) => Ok(()),
         Err(_) => Err(format!("expected an integer, got `{}`", s)),
     }
@@ -1617,8 +1617,8 @@ pub fn bounded_int_validator(s: String, lo: usize, hi: usize) -> Result<(), Stri
 
 /// Validates boolean input.
 #[cfg_attr(feature = "cargo-clippy", allow(needless_pass_by_value))]
-pub fn bool_validator(s: String) -> Result<(), String> {
-    if bool_of_str(&s).is_some() {
+pub fn bool_validator(s: &str) -> Result<(), String> {
+    if bool_of_str(s).is_some() {
         Ok(())
     } else {
         Err(format!("expected `on/true` or `off/false`, got `{}`", s))
diff --git a/src/common/msg.rs b/src/common/msg.rs
index 39a06add..f5b08e5e 100644
--- a/src/common/msg.rs
+++ b/src/common/msg.rs
@@ -36,13 +36,13 @@ impl Id {
         }
     }
 }
-impl_fmt! {
-  Id(self, fmt) {
-    match * self {
-      Id::Learner(idx) => write!(fmt, "learner#{}", idx),
-      Id::Assistant => write!(fmt, "assistant"),
+impl fmt::Display for Id {
+    fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
+        match *self {
+            Id::Learner(idx) => write!(fmt, "learner#{}", idx),
+            Id::Assistant => write!(fmt, "assistant"),
+        }
     }
-  }
 }
 
 /// Kind of messages the teacher can receive.
diff --git a/src/data.rs b/src/data.rs
index bd727db6..380ab014 100644
--- a/src/data.rs
+++ b/src/data.rs
@@ -245,11 +245,11 @@ impl LrnData {
     ///   (mc91 3 0)
     /// ) neg (
     /// ) constraints (
-    ///   0 | (mc91 2 102) (mc91 1 101) => (mc91 7 3)
-    ///   1 | (mc91 2 102) (mc91 1 101) => (dummy 7 3)
+    ///   0 | (mc91 1 101) (mc91 2 102) => (mc91 7 3)
+    ///   1 | (mc91 1 101) (mc91 2 102) => (dummy 7 3)
     /// ) constraint map(
-    ///   (mc91 7 3) -> 0
     ///   (mc91 2 102) -> 0 1
+    ///   (mc91 7 3) -> 0
     ///   (mc91 1 101) -> 0 1
     ///   (dummy 7 3) -> 1
     /// ) positive examples staged (
@@ -394,11 +394,11 @@ impl LrnData {
     ///   (mc91 3 0)
     /// ) neg (
     /// ) constraints (
-    ///   0 | (mc91 2 102) (mc91 1 101) => (mc91 7 3)
-    ///   1 | (mc91 2 102) (mc91 1 101) => (dummy 7 3)
+    ///   0 | (mc91 1 101) (mc91 2 102) => (mc91 7 3)
+    ///   1 | (mc91 1 101) (mc91 2 102) => (dummy 7 3)
     /// ) constraint map(
-    ///   (mc91 7 3) -> 0
     ///   (mc91 2 102) -> 0 1
+    ///   (mc91 7 3) -> 0
     ///   (mc91 1 101) -> 0 1
     ///   (dummy 7 3) -> 1
     /// ) positive examples staged (
@@ -518,11 +518,11 @@ impl LrnData {
     ///   (mc91 3 0)
     /// ) neg (
     /// ) constraints (
-    ///   0 | (mc91 2 102) (mc91 1 101) => (mc91 7 3)
-    ///   1 | (mc91 2 102) (mc91 1 101) => (dummy 7 3)
+    ///   0 | (mc91 1 101) (mc91 2 102) => (mc91 7 3)
+    ///   1 | (mc91 1 101) (mc91 2 102) => (dummy 7 3)
     /// ) constraint map(
-    ///   (mc91 7 3) -> 0
     ///   (mc91 2 102) -> 0 1
+    ///   (mc91 7 3) -> 0
     ///   (mc91 1 101) -> 0 1
     ///   (dummy 7 3) -> 1
     /// ) positive examples staged (
@@ -1495,10 +1495,10 @@ impl Data {
     ///   (mc91 3 0)
     /// ) neg (
     /// ) constraints (
-    ///   0 | (mc91 2 102) (mc91 1 101) => (mc91 7 3)
+    ///   0 | (mc91 1 101) (mc91 2 102) => (mc91 7 3)
     /// ) constraint map(
-    ///   (mc91 7 3) -> 0
     ///   (mc91 2 102) -> 0
+    ///   (mc91 7 3) -> 0
     ///   (mc91 1 101) -> 0
     /// ) positive examples staged (
     ///   mc91 | (1 101)

From 7fc17ca6571d35530d5e95fb836e1fe7aa576f32 Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Mon, 16 May 2022 01:58:21 +0200
Subject: [PATCH 4/6] update rsmt2 dep

---
 Cargo.lock        | 4 ++--
 Cargo.toml        | 2 +-
 src/common/smt.rs | 8 ++++----
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index d774db5d..d2b82de2 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -358,9 +358,9 @@ dependencies = [
 
 [[package]]
 name = "rsmt2"
-version = "0.12.0"
+version = "0.16.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b616b1ac7f0393f4441a0d6301b35b1bccd209c61dd65c8852cb8397d68cdc89"
+checksum = "c45b1d4532681fdeedf72363ce5b4580a03b1eab4febe5a89f4aebf521319b16"
 dependencies = [
  "error-chain",
 ]
diff --git a/Cargo.toml b/Cargo.toml
index d12e8814..1541a1f1 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -38,7 +38,7 @@ clap = { version = "*", features = ["cargo"] }
 hashconsing = { path = "../hashconsing" }
 error-chain = "*"
 ansi_term = "*"
-rsmt2 = "^0.12"
+rsmt2 = "^0.16"
 num = "*"
 mylib = { git = "https://github.com/AdrienChampion/mylib" }
 either = "*"
diff --git a/src/common/smt.rs b/src/common/smt.rs
index cb4dce78..6116046e 100644
--- a/src/common/smt.rs
+++ b/src/common/smt.rs
@@ -745,10 +745,10 @@ impl FullParser {
                             if let Some((sig, def)) = fun_defs.get(&fun) {
                                 debug_assert_eq! { sig.len(), 1 }
                                 let idx_type = sig.iter().next().unwrap();
-                                let array =
-                                    val::array_of_fun(idx_type.clone(), def).chain_err(|| {
-                                        "while recovering array from function definition"
-                                    })?;
+                                let array = rsmt2::prelude::ResExt::chain_err(
+                                    val::array_of_fun(idx_type.clone(), def),
+                                    || "while recovering array from function definition",
+                                )?;
                                 res.push((var, typ, array))
                             } else {
                                 postponed.push((FPVar::Var(var), sig, typ, FPVal::FunToArray(fun)))

From f568de10e89a8ef6baf768f69374399bc9fa1fa4 Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Mon, 16 May 2022 03:17:54 +0200
Subject: [PATCH 5/6] updated hashconsing

---
 Cargo.lock            |   6 ++-
 Cargo.toml            |   4 +-
 rsc/sat/issue_57.smt2 | 117 ++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 123 insertions(+), 4 deletions(-)
 create mode 100644 rsc/sat/issue_57.smt2

diff --git a/Cargo.lock b/Cargo.lock
index d2b82de2..dc4efbad 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -142,7 +142,9 @@ checksum = "ab5ef0d4909ef3724cc8cce6ccc8572c5c817592e9285f5464f8e86f8bd3726e"
 
 [[package]]
 name = "hashconsing"
-version = "1.5.0"
+version = "1.5.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a7676ca96091e9e4634fbf9d179c65e0ba8c70323fdedbbe4a14d9dd3f3746c1"
 dependencies = [
  "lazy_static",
 ]
@@ -158,7 +160,7 @@ dependencies = [
 
 [[package]]
 name = "hoice"
-version = "1.9.0"
+version = "1.10.0"
 dependencies = [
  "ansi_term",
  "atty",
diff --git a/Cargo.toml b/Cargo.toml
index 1541a1f1..9e4a92e9 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "hoice"
-version = "1.9.0"
+version = "1.10.0"
 authors = ["Adrien Champion <adrien.champion@email.com>"]
 description = "A ICE-based Horn clause solver."
 homepage = "https://github.com/hopv/hoice"
@@ -35,7 +35,7 @@ bench = [ ]
 libc = "*"
 lazy_static = "*"
 clap = { version = "*", features = ["cargo"] }
-hashconsing = { path = "../hashconsing" }
+hashconsing = "*"
 error-chain = "*"
 ansi_term = "*"
 rsmt2 = "^0.16"
diff --git a/rsc/sat/issue_57.smt2 b/rsc/sat/issue_57.smt2
new file mode 100644
index 00000000..24de6768
--- /dev/null
+++ b/rsc/sat/issue_57.smt2
@@ -0,0 +1,117 @@
+(set-logic HORN)
+
+(declare-fun
+  main@_6
+  ( Int Int Int ) Bool
+)
+(declare-fun
+  main@.preheader
+  ( Int Int Int Int ) Bool
+)
+(declare-fun
+  main@.lr.ph
+  ( Int Int ) Bool
+)
+
+(assert 
+  (forall
+    ( (A Int) (C Int) (I Int) (J Int) )
+    (=>
+      (and
+        (>= (+ C (* (- 1) J)) 0) (>= (+ I (* (- 1) A)) 1)
+        (main@.preheader C A I J)
+      )
+      (main@.preheader (+ C (- 1)) (+ A 1) I J)
+    )
+  )
+)
+
+(assert 
+  (forall
+    ( (H Int) (I Int) )
+    (=>
+      (and
+        true
+        true
+      )
+      (main@_6 0 H I)
+    )
+  )
+)
+
+(assert 
+  (forall
+    ( (A Int) (B Int) (D Int) )
+    (=>
+      (and
+        (not (= D 0))
+        (main@.lr.ph A B)
+      )
+      (main@.lr.ph (+ A 1) (+ B 1))
+    )
+  )
+)
+
+(assert 
+  (forall
+    ( (B Int) (C Int) (L Int) (M Int) )
+    (=>
+      (and
+        (not (= B 0))
+        (main@_6 C L M)
+      )
+      (main@_6 (+ C 1) L M)
+    )
+  )
+)
+
+(assert 
+  (forall
+    ( (B Int) (C Int) (D Int) )
+    (=>
+      (and
+        (or (>= (+ C (* (- 1) B)) 1) (>= (+ D (* (- 1) C)) 0))
+        (main@_6 C B D)
+      )
+      (main@.preheader 0 0 (- 1) 1)
+    )
+  )
+)
+
+(assert 
+  (forall
+    ( (A Int) (B Int) (C Int) (H Int) )
+    (=>
+      (and
+        (or (>= (+ B (* (- 1) A)) 1) (>= (+ C (* (- 1) B)) 0)) (not (= H 0))
+        (main@_6 B A C)
+      )
+      (main@.lr.ph 0 0)
+    )
+  )
+)
+(assert 
+  (forall
+    ( (A Int) (C Int) (D Int) (G Int) )
+    (=>
+      (and
+        (>= (+ G (* (- 1) A)) 2) (>= (+ D (* (- 1) C)) 1)
+        (main@.preheader (+ A 1) C D G)
+      )
+      false
+    )
+  )
+)
+(assert 
+  (forall
+    ( (B Int) (I Int) )
+    (=>
+      (and
+        true
+        (main@.lr.ph I B)
+      )
+      (main@.preheader (+ B 1) 0 I 1)
+    )
+  )
+)
+(check-sat)

From b6dd940c4a53c374a5933d9945a4f068f2839844 Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Mon, 16 May 2022 03:20:54 +0200
Subject: [PATCH 6/6] bump for obsolete ci

---
 Cargo.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cargo.toml b/Cargo.toml
index 9e4a92e9..8c102fb4 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -35,7 +35,7 @@ bench = [ ]
 libc = "*"
 lazy_static = "*"
 clap = { version = "*", features = ["cargo"] }
-hashconsing = "*"
+hashconsing = "^1"
 error-chain = "*"
 ansi_term = "*"
 rsmt2 = "^0.16"