5 files changed, 25 insertions, 9 deletions
diff --git a/metadata/md5-cache/sci-mathematics/Manifest.gz b/metadata/md5-cache/sci-mathematics/Manifest.gz
index 9c74b0197c74..e2c5a6ca8cbb 100644
--- a/metadata/md5-cache/sci-mathematics/Manifest.gz
+++ b/metadata/md5-cache/sci-mathematics/Manifest.gz
diff --git a/metadata/md5-cache/sci-mathematics/boolector-3.2.3 b/metadata/md5-cache/sci-mathematics/boolector-3.2.3
new file mode 100644
index 000000000000..fb784f7b8ec5
--- /dev/null
+++ b/metadata/md5-cache/sci-mathematics/boolector-3.2.3
@@ -0,0 +1,17 @@
+BDEPEND=test? ( dev-cpp/gtest ) >=dev-util/ninja-1.8.2 >=dev-util/cmake-3.20.5
+DEFINED_PHASES=compile configure install prepare setup test
+DEPEND=sci-mathematics/btor2tools:= cryptominisat? ( sci-mathematics/cryptominisat:= ) gmp? ( dev-libs/gmp:= ) minisat? ( sci-mathematics/minisat:= ) picosat? ( sci-mathematics/picosat:= ) python? ( python_single_target_python3_10? ( dev-lang/python:3.10 ) python_single_target_python3_11? ( dev-lang/python:3.11 ) python_single_target_python3_12? ( dev-lang/python:3.12 ) )
+DESCRIPTION=Fast SMT solver for bit-vectors, arrays and uninterpreted functions
+EAPI=8
+HOMEPAGE=https://boolector.github.io/ https://github.com/Boolector/boolector/
+INHERIT=python-single-r1 cmake
+IUSE=cryptominisat examples +gmp minisat +picosat python test python_single_target_python3_10 python_single_target_python3_11 python_single_target_python3_12
+KEYWORDS=~amd64 ~x86
+LICENSE=MIT
+RDEPEND=sci-mathematics/btor2tools:= cryptominisat? ( sci-mathematics/cryptominisat:= ) gmp? ( dev-libs/gmp:= ) minisat? ( sci-mathematics/minisat:= ) picosat? ( sci-mathematics/picosat:= ) python? ( python_single_target_python3_10? ( dev-lang/python:3.10 ) python_single_target_python3_11? ( dev-lang/python:3.11 ) python_single_target_python3_12? ( dev-lang/python:3.12 ) )
+REQUIRED_USE=python? ( ^^ ( python_single_target_python3_10 python_single_target_python3_11 python_single_target_python3_12 ) ) || ( cryptominisat minisat picosat )
+RESTRICT=!test? ( test )
+SLOT=0
+SRC_URI=https://github.com/Boolector/boolector/archive/3.2.3.tar.gz -> boolector-3.2.3.tar.gz
+_eclasses_=cmake	0f2e0c197fad0312f3c4765c9cf36271	flag-o-matic	baa4d385108ac87993edac956a916a36	multilib	c19072c3cd7ac5cb21de013f7e9832e0	multiprocessing	30ead54fa2e2b5f9cd4e612ffc34d0fe	ninja-utils	39e7a84b06eff4efd9f2e0c3d1668b98	python-single-r1	75118e916668a74c660a13b0ecb22562	python-utils-r1	f6221c2f55e5e832be9919fe1711f33b	toolchain-funcs	70ec42843fec87d20fd94c67e77cdbff	xdg-utils	baea6080dd821f5562d715887954c9d3
+_md5_=ad336050dcbbf804e08b446da6b4e98d
diff --git a/metadata/md5-cache/sci-mathematics/btor2tools-1.0.0_pre20220518-r1 b/metadata/md5-cache/sci-mathematics/btor2tools-1.0.0_pre20220518-r1
index f87e32cbce7d..9d38a99da230 100644
--- a/metadata/md5-cache/sci-mathematics/btor2tools-1.0.0_pre20220518-r1
+++ b/metadata/md5-cache/sci-mathematics/btor2tools-1.0.0_pre20220518-r1
@@ -10,4 +10,4 @@ LICENSE=MIT
 SLOT=0
 SRC_URI=https://github.com/Boolector/btor2tools/archive/b8456dda4780789e882f5791eb486f295ade4da4.tar.gz -> btor2tools-1.0.0_pre20220518.tar.gz
 _eclasses_=cmake	0f2e0c197fad0312f3c4765c9cf36271	flag-o-matic	baa4d385108ac87993edac956a916a36	multilib	c19072c3cd7ac5cb21de013f7e9832e0	multiprocessing	30ead54fa2e2b5f9cd4e612ffc34d0fe	ninja-utils	39e7a84b06eff4efd9f2e0c3d1668b98	toolchain-funcs	70ec42843fec87d20fd94c67e77cdbff	xdg-utils	baea6080dd821f5562d715887954c9d3
-_md5_=c276ec66337a42e48e2194b4a977133c
+_md5_=c06b31273fb972eaf396c38e9b2c0a6f
diff --git a/metadata/md5-cache/sci-mathematics/proverif-2.04 b/metadata/md5-cache/sci-mathematics/proverif-2.04-r1
index 6d16dedf23af..f0eb0b81b1f8 100644
--- a/metadata/md5-cache/sci-mathematics/proverif-2.04
+++ b/metadata/md5-cache/sci-mathematics/proverif-2.04-r1
@@ -1,6 +1,5 @@
-BDEPEND=emacs? ( >=app-editors/emacs-25:* )
 DEFINED_PHASES=compile install test
-DEPEND=>=dev-ml/findlib-1.0.4-r1[ocamlopt?]
+DEPEND=dev-lang/ocaml:=[ocamlopt] emacs? ( >=app-editors/emacs-25:* ) >=dev-ml/findlib-1.0.4-r1[ocamlopt?]
 DESCRIPTION=Cryptographic protocol verifier in the formal model
 EAPI=8
 HOMEPAGE=https://bblanche.gitlabpages.inria.fr/proverif/ https://gitlab.inria.fr/bblanche/proverif/
@@ -8,8 +7,8 @@ INHERIT=edo elisp-common findlib
 IUSE=emacs +ocamlopt
 KEYWORDS=~amd64 ~x86
 LICENSE=GPL-2+
-RDEPEND=emacs? ( >=app-editors/emacs-25:* ) dev-lang/ocaml:=[ocamlopt?]
+RDEPEND=dev-lang/ocaml:=[ocamlopt] emacs? ( >=app-editors/emacs-25:* ) dev-lang/ocaml:=[ocamlopt?]
 SLOT=0
 SRC_URI=https://gitlab.inria.fr/bblanche/proverif/-/archive/v2.04/proverif-v2.04.tar.bz2
 _eclasses_=edo	c0eb9cbe6b0bd01fcb4918f12598a4d3	elisp-common	2a0fa407d2e6363c663ccb299503b25c	findlib	cc1c14904708a0a28bcb256b342a808c
-_md5_=5d8b3e45511fdfc3880f0e1de2393978
+_md5_=167673677120928bfde7755df17218b3
diff --git a/metadata/md5-cache/sci-mathematics/proverif-9999 b/metadata/md5-cache/sci-mathematics/proverif-9999
index 7b87c5c093a3..3d0d71d0b2fd 100644
--- a/metadata/md5-cache/sci-mathematics/proverif-9999
+++ b/metadata/md5-cache/sci-mathematics/proverif-9999
@@ -1,6 +1,6 @@
-BDEPEND=emacs? ( >=app-editors/emacs-25:* ) >=dev-vcs/git-1.8.2.1[curl]
+BDEPEND=>=dev-vcs/git-1.8.2.1[curl]
 DEFINED_PHASES=compile install test unpack
-DEPEND=>=dev-ml/findlib-1.0.4-r1[ocamlopt?]
+DEPEND=dev-lang/ocaml:=[ocamlopt] emacs? ( >=app-editors/emacs-25:* ) >=dev-ml/findlib-1.0.4-r1[ocamlopt?]
 DESCRIPTION=Cryptographic protocol verifier in the formal model
 EAPI=8
 HOMEPAGE=https://bblanche.gitlabpages.inria.fr/proverif/ https://gitlab.inria.fr/bblanche/proverif/
@@ -8,7 +8,7 @@ INHERIT=edo elisp-common findlib git-r3
 IUSE=emacs +ocamlopt
 LICENSE=GPL-2+
 PROPERTIES=live
-RDEPEND=emacs? ( >=app-editors/emacs-25:* ) dev-lang/ocaml:=[ocamlopt?]
+RDEPEND=dev-lang/ocaml:=[ocamlopt] emacs? ( >=app-editors/emacs-25:* ) dev-lang/ocaml:=[ocamlopt?]
 SLOT=0
 _eclasses_=edo	c0eb9cbe6b0bd01fcb4918f12598a4d3	elisp-common	2a0fa407d2e6363c663ccb299503b25c	findlib	cc1c14904708a0a28bcb256b342a808c	git-r3	2358a7b20091609e24bd3a83b3ac5991
-_md5_=5d8b3e45511fdfc3880f0e1de2393978
+_md5_=167673677120928bfde7755df17218b3