From nobody Fri Feb  2 00:05:00 2024
X-Original-To: dev-commits-ports-main@mlmmj.nyi.freebsd.org
Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1])
	by mlmmj.nyi.freebsd.org (Postfix) with ESMTP id 4TQwyD1Hfmz58yPt
	for <dev-commits-ports-main@mlmmj.nyi.freebsd.org>; Fri,  2 Feb 2024 00:05:08 +0000 (UTC)
	(envelope-from daniel.engberg.lists@pyret.net)
Received: from smtp-bc0c.mail.infomaniak.ch (smtp-bc0c.mail.infomaniak.ch [IPv6:2001:1600:4:17::bc0c])
	(using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)
	 key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256
	 client-signature RSA-PSS (2048 bits) client-digest SHA256)
	(Client CN "relay.mail.infomaniak.ch", Issuer "R3" (verified OK))
	by mx1.freebsd.org (Postfix) with ESMTPS id 4TQwyC1Tdyz3xWS;
	Fri,  2 Feb 2024 00:05:07 +0000 (UTC)
	(envelope-from daniel.engberg.lists@pyret.net)
Authentication-Results: mx1.freebsd.org;
	none
Received: from smtp-3-0000.mail.infomaniak.ch (unknown [10.4.36.107])
	by smtp-3-3000.mail.infomaniak.ch (Postfix) with ESMTPS id 4TQwy52bywzMqcXP;
	Fri,  2 Feb 2024 01:05:01 +0100 (CET)
Received: from unknown by smtp-3-0000.mail.infomaniak.ch (Postfix) with ESMTPA id 4TQwy46RSwz3Y;
	Fri,  2 Feb 2024 01:05:00 +0100 (CET)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=pyret.net;
	s=20231006; t=1706832301;
	bh=7hY96Vrytij6DJ+OvTAPIzpIAdxUbLzTkGeP5VmH8Jk=;
	h=Date:Subject:From:Reply-To:To:Cc:References:In-Reply-To:From;
	b=NZJHcCx45U7lDjEZTHU78A+Ev+F7OBPD1JaM8pn6qWjmjIlHDiubH4kbIfDDafzc9
	 3Oc8kDiIyTh0Z5r5CQSg8PUIcPq9wdW5uLgPnuRA/ARrvV+WHcb3RQqWPTL5VZTvzN
	 r2zv3ekUUKG+cmz7uq6vt9uRmYyfV0VJ1ztyt6XzhsYFbicK/s5WY5iqZv1lqzhEKH
	 AvnOGuhYkKvy7gOSuDjvujH9QM4GvPty5Xk+cxgpY3+1I5uBTe68IidChZA3ycMV3J
	 m+Wh+nVUVwtf1bAyQCVhfJoCwGmI34FurIWRc4eJmaKxkhwjKjjoLKrKHdpidjhlcu
	 UR7C122d49uWQ==
Message-ID: <379c7ddb410058469dcda4f67b45caa9@mail.infomaniak.com>
Date: Fri, 02 Feb 2024 01:05:00 +0100
Subject: Re: git: 7f087b720e52 - main - devel/cbmc: add new port
From: Daniel Engberg <daniel.engberg.lists@pyret.net>
Reply-To: Daniel Engberg <daniel.engberg.lists@pyret.net>
To: Olivier Cochard <olivier@FreeBSD.org>
Cc: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org,
 dev-commits-ports-main@FreeBSD.org
List-Id: Commits to the main branch of the FreeBSD ports repository <dev-commits-ports-main.freebsd.org>
List-Archive: https://lists.freebsd.org/archives/dev-commits-ports-main
List-Help: <mailto:dev-commits-ports-main+help@freebsd.org>
List-Post: <mailto:dev-commits-ports-main@freebsd.org>
List-Subscribe: <mailto:dev-commits-ports-main+subscribe@freebsd.org>
List-Unsubscribe: <mailto:dev-commits-ports-main+unsubscribe@freebsd.org>
Sender: owner-dev-commits-ports-main@freebsd.org
X-BeenThere: dev-commits-ports-main@freebsd.org
MIME-Version: 1.0
Content-Type: multipart/alternative;
 boundary="_=_swift_1706832300_c2dcb94f2c2cc263794507f6574d26b4_=_"
X-WS-User-Origin: eyJpdiI6Im5XdUx3c3RqNCtaTVlUeTRzV2tYL0E9PSIsInZhbHVlIjoiaGE2eWc3MWpxbG8xMnZmV0hhQ2pBUT09IiwibWFjIjoiYzYzNDQxM2FhNjJhZDUzODA4NGM3M2Y2NDliYjE3MjU1ZTgzZDJhZTdiZGY2YWY0Y2E5MzFmYzBmNTdhNDE4YSIsInRhZyI6IiJ9
X-WS-User-Mbox: eyJpdiI6ImRHOWRwYUpSNXdLS3E3ME1GeldNTVE9PSIsInZhbHVlIjoiNVhWdU1LbSs5U0lDZ3ZxZHJLejJoZz09IiwibWFjIjoiZGM4MmQzZTUxYWEyMmI4NjM4NGJkYjA2NzdmOTUxOTJlM2RhODA1ZGU2ZDdmMjgxNDVhZDUyMTU2ZmUyMmQyNiIsInRhZyI6IiJ9
X-WS-Location: eJxzKUpMKykGAAfpAmU-
X-Mailer: Infomaniak Workspace (1.3.633)
References: <202402011755.411Ht9G8016149@gitrepo.freebsd.org>
In-Reply-To: <202402011755.411Ht9G8016149@gitrepo.freebsd.org>
X-Infomaniak-Routing: alpha
X-Rspamd-Queue-Id: 4TQwyC1Tdyz3xWS
X-Spamd-Bar: ----
X-Rspamd-Pre-Result: action=no action;
	module=replies;
	Message is reply to one we originated
X-Spamd-Result: default: False [-4.00 / 15.00];
	REPLY(-4.00)[];
	ASN(0.00)[asn:29222, ipnet:2001:1600::/32, country:CH]


--_=_swift_1706832300_c2dcb94f2c2cc263794507f6574d26b4_=_
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable

On 2024-02-01T18:55:09.000+01:00, Olivier Cochard
<olivier@FreeBSD.org> w=
rote:

>=C2=A0The=C2=A0branch=C2=A0main=C2=A0has=C2=A0been=C2=A0updated=
=C2=A0by=C2=A0olivier:
>=C2=A0
>=C2=A0URL:=C2=A0https://cgit.FreeBSD.or=
g/ports/commit/?id=3D7f087b720e52d51b22db0da2d7565418a0e428ef
>=C2=A0
>=
=C2=A0commit=C2=A07f087b720e52d51b22db0da2d7565418a0e428ef
>=C2=A0
>=
=C2=A0Author:=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0Olivier=C2=A0Cochard=C2=A0<olivi=
er@FreeBSD.org>
>=C2=A0
>=C2=A0AuthorDate:=C2=A02024-02-01=C2=A017:50:0=
2=C2=A0+0000
>=C2=A0
>=C2=A0Commit:=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0Olivie=
r=C2=A0Cochard=C2=A0<olivier@FreeBSD.org>
>=C2=A0
>=C2=A0CommitDate:=
=C2=A02024-02-01=C2=A017:53:55=C2=A0+0000
>=C2=A0
>=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0devel/cbmc:=C2=A0add=C2=A0new=C2=A0port
>=C2=A0
>=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0
>=C2=A0
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0Boun=
ded=C2=A0Model=C2=A0Checker=C2=A0for=C2=A0C=C2=A0and=C2=A0C++=C2=A0programs=

>=C2=A0
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0https://github.com/diffblue/cbm=
c
>=C2=A0
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0
>=C2=A0
>=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0Sponsored=C2=A0by:=C2=A0=C2=A0=C2=A0Netflix
>=C2=A0
>=
=C2=A0---
>=C2=A0
>=C2=A0=C2=A0devel/Makefile=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A0=C2=A01=
=C2=A0+
>=C2=A0
>=C2=A0=C2=A0devel/cbmc/Makefile=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A046=C2=A0+++++++++++++++++
>=C2=A0
=
>=C2=A0=C2=A0devel/cbmc/distinfo=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0|=C2=A0=C2=A05=C2=A0++
>=C2=A0
>=C2=A0=C2=A0.../patch-minisat-=
2.2.1_minisat_core_Solver.cc=C2=A0[http://Solver.cc]=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0|=C2=A020=C2=A0++++++++
>=C2=A0
>=C2=A0=C2=A0.../patch-mini=
sat-2.2.1_minisat_core_SolverTypes.h=C2=A0|=C2=A059=C2=A0++++++++++++++++++=
++++
>=C2=A0
>=C2=A0=C2=A0.../patch-minisat-2.2.1_minisat_mtl_IntTypes.=
h=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A012=C2=A0+++++
>=C2=A0
>=C2=A0=
=C2=A0.../files/patch-minisat-2.2.1_minisat_mtl_Vec.h=C2=A0=C2=A0=C2=A0=
=C2=A0|=C2=A016=C2=A0++++++
>=C2=A0
>=C2=A0=C2=A0.../files/patch-minisa=
t-2.2.1_minisat_mtl_XAlloc.h=C2=A0|=C2=A019=C2=A0+++++++
>=C2=A0
>=
=C2=A0=C2=A0.../patch-minisat-2.2.1_minisat_simp_SimpSolver.cc=C2=A0[http:/=
/SimpSolver.cc]=C2=A0|=C2=A037=C2=A0++++++++++++++
>=C2=A0
>=C2=A0=
=C2=A0.../patch-minisat-2.2.1_minisat_utils_Options.cc=C2=A0[http://Options=
.cc]=C2=A0=C2=A0=C2=A0|=C2=A015=C2=A0++++++
>=C2=A0
>=C2=A0=C2=A0.../pa=
tch-minisat-2.2.1_minisat_utils_Options.h=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A030=
=C2=A0+++++++++++
>=C2=A0
>=C2=A0=C2=A0.../patch-minisat-2.2.1_minisat_=
utils_ParseUtils.h=C2=A0|=C2=A033=C2=A0++++++++++++
>=C2=A0
>=C2=A0=
=C2=A0.../patch-minisat-2.2.1_minisat_utils_System.h=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0|=C2=A011=C2=A0++++
>=C2=A0
>=C2=A0=C2=A0devel/cbmc/files/p=
atch-src_common=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A011=C2=A0++++
>=
=C2=A0
>=C2=A0=C2=A0.../files/patch-src_solvers_sat_external__sat.cpp=
=C2=A0=C2=A0|=C2=A013=C2=A0+++++
>=C2=A0
>=C2=A0=C2=A0devel/cbmc/files/=
patch-src_util_optional.h=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0|=C2=A029=C2=A0+++++++++++
>=C2=A0
>=C2=A0=C2=A0devel/cbmc/pkg=
-descr=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A0=C2=A07=C2=A0+++
>=
=C2=A0
>=C2=A0=C2=A0devel/cbmc/pkg-plist=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0|=C2=A023=C2=A0+++++++++
>=C2=A0
>=C2=A0=C2=A018=C2=A0files=
=C2=A0changed,=C2=A0387=C2=A0insertions(+)
>=C2=A0
>=C2=A0diff=C2=A0--g=
it=C2=A0a/devel/Makefile=C2=A0b/devel/Makefile
>=C2=A0
>=C2=A0index=
=C2=A04da71e0953a1..51481c8a3aca=C2=A0100644
>=C2=A0
>=C2=A0---=C2=
=A0a/devel/Makefile
>=C2=A0
>=C2=A0+++=C2=A0b/devel/Makefile
>=C2=
=A0
>=C2=A0@@=C2=A0-351,6=C2=A0+351,7=C2=A0@@
>=C2=A0
>=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=C2=A0+=3D=C2=A0catch2
>=C2=A0
>=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=C2=A0+=3D=C2=A0cbang
>=C2=A0
>=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=C2=A0+=3D=C2=A0cbfmt
>=C2=
=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=C2=A0+=3D=C2=A0cbmc
>=C2=
=A0
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=C2=A0+=3D=C2=A0cbrowser=

>=C2=A0
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=C2=A0+=3D=C2=A0cc6=
5
>=C2=A0
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=C2=A0+=3D=C2=
=A0ccache
>=C2=A0
>=C2=A0diff=C2=A0--git=C2=A0a/devel/cbmc/Makefile=
=C2=A0b/devel/cbmc/Makefile
>=C2=A0
>=C2=A0new=C2=A0file=C2=A0mode=
=C2=A0100644
>=C2=A0
>=C2=A0index=C2=A0000000000000..c7f7b3650e63
>=
=C2=A0
>=C2=A0---=C2=A0/dev/null
>=C2=A0
>=C2=A0+++=C2=A0b/devel/cbmc=
/Makefile
>=C2=A0
>=C2=A0@@=C2=A0-0,0=C2=A0+1,46=C2=A0@@
>=C2=A0
>=
=C2=A0+PORTNAME=3D=C2=A0=C2=A0=C2=A0=C2=A0cbmc
>=C2=A0
>=C2=A0+PORTVERS=
ION=3D=C2=A0=C2=A0=C2=A0=C2=A05.95.1
>=C2=A0
>=C2=A0+DISTVERSIONPREFIX=
=3D=C2=A0=C2=A0=C2=A0=C2=A0cbmc-
>=C2=A0
>=C2=A0+CATEGORIES=3D=C2=A0=
=C2=A0=C2=A0=C2=A0devel
>=C2=A0
>=C2=A0+MASTER_SITES=3D=C2=A0=C2=A0=
=C2=A0=C2=A0DEBIAN/pool/main/m/minisat2:minisat
>=C2=A0
>=C2=A0+DISTFIL=
ES=3D=C2=A0=C2=A0=C2=A0=C2=A0minisat2_2.2.1.orig.tar.gz:minisat
>=C2=
=A0
>=C2=A0+
>=C2=A0
>=C2=A0+MAINTAINER=3D=C2=A0=C2=A0=C2=A0=C2=A0oli=
vier@FreeBSD.org
>=C2=A0
>=C2=A0+COMMENT=3D=C2=A0=C2=A0=C2=A0=C2=A0Boun=
ded=C2=A0Model=C2=A0Checker=C2=A0for=C2=A0C=C2=A0and=C2=A0C++=C2=A0programs=

>=C2=A0
>=C2=A0+WWW=3D=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0https://github.com/diffblue/cbmc
>=C2=A0
>=C2=A0+
>=C2=A0
>=
=C2=A0+LICENSE=3D=C2=A0=C2=A0=C2=A0=C2=A0BSD4CLAUSE
>=C2=A0
>=C2=A0+LIC=
ENSE_FILE=3D=C2=A0=C2=A0=C2=A0=C2=A0${WRKSRC}/LICENSE
>=C2=A0
>=C2=
=A0+
>=C2=A0
>=C2=A0+BUILD_DEPENDS=3D=C2=A0=C2=A0=C2=A0=C2=A0${LOCALBAS=
E}/bin/flex:textproc/flex
>=C2=A0
>=C2=A0+RUN_DEPENDS=3D=C2=A0=C2=A0=
=C2=A0=C2=A0${LOCALBASE}/bin/cvc5:math/cvc5=C2=A0\
>=C2=A0
>=C2=A0+=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0${LOCALBASE}/bin/z3:math/z3=

>=C2=A0
>=C2=A0+
>=C2=A0
>=C2=A0+USES=3D=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0gmake=C2=A0bison=C2=A0python=C2=A0shebangfix
>=
=C2=A0
>=C2=A0+
>=C2=A0
>=C2=A0+USE_GITHUB=3D=C2=A0=C2=A0=C2=A0=C2=
=A0yes
>=C2=A0
>=C2=A0+GH_ACCOUNT=3D=C2=A0=C2=A0=C2=A0=C2=A0diffblue
=
>=C2=A0
>=C2=A0+SHEBANG_FILES=3D=C2=A0=C2=A0=C2=A0=C2=A0${WRKSRC}/scripts=
/ls_parse.py=C2=A0[http://parse.py]
>=C2=A0
>=C2=A0+WRKSRC_minisat=3D=
=C2=A0=C2=A0=C2=A0=C2=A0${WRKDIR}/minisat2-2.2.1
>=C2=A0
>=C2=A0+
>=
=C2=A0
>=C2=A0+post-patch:
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=
=A0@${REINPLACE_CMD}=C2=A0-e=C2=A0's|.*git=C2=A0describe=C2=A0--tags.*|GIT_=
INFO=C2=A0=3D=C2=A0${PORTNAME}-${PORTVERSION}|'=C2=A0\
>=C2=A0
>=C2=
=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0${WRKSRC}/src/util/Make=
file
>=C2=A0
>=C2=A0+post-extract:
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=
=C2=A0=C2=A0@${MV}=C2=A0${WRKSRC_minisat}=C2=A0${WRKSRC}/minisat-2.2.1
>=
=C2=A0
>=C2=A0+
>=C2=A0
>=C2=A0+do-build:
>=C2=A0
>=C2=A0+=C2=
=A0=C2=A0=C2=A0=C2=A0@${MKDIR}=C2=A0${STAGEDIR}
>=C2=A0
>=C2=A0+=C2=
=A0=C2=A0=C2=A0=C2=A0cd=C2=A0${WRKSRC}=C2=A0&&=C2=A0${GMAKE}=C2=A0-C=C2=
=A0src=C2=A0-j${MAKE_JOBS_NUMBER}
>=C2=A0
>=C2=A0+
>=C2=A0
>=C2=
=A0+do-install:
>=C2=A0
>=C2=A0+.=C2=A0=C2=A0for=C2=A0x=C2=A0in=C2=
=A0cbmc=C2=A0crangler=C2=A0goto-analyzer=C2=A0goto-cc=C2=A0goto-diff=C2=
=A0goto-instrument=C2=A0\
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0goto-=
inspect=C2=A0goto-harness=C2=A0goto-synthesizer=C2=A0symtab2gb
>=C2=A0
=
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${INSTALL_PROGRAM}=C2=A0${WRKSRC}/src/${x}/=
${x}=C2=A0${STAGEDIR}${PREFIX}/bin/
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=
=A0=C2=A0${INSTALL_MAN}=C2=A0${WRKSRC}/doc/man/${x}.1=C2=A0${STAGEDIR}${PRE=
FIX}/share/man/man1/
>=C2=A0
>=C2=A0+.=C2=A0=C2=A0endfor
>=C2=A0
>=
=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${LN}=C2=A0-sf=C2=A0goto-cc=C2=A0${STAGEDIR}=
${PREFIX}/bin/goto-gcc
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${LN}=
=C2=A0-sf=C2=A0goto-cc=C2=A0${STAGEDIR}${PREFIX}/bin/goto-ld
>=C2=A0
>=
=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${INSTALL_SCRIPT}=C2=A0${WRKSRC}/scripts/ls_=
parse.py=C2=A0[http://parse.py]=C2=A0${STAGEDIR}${PREFIX}/bin/
>=C2=A0
=
>=C2=A0+
>=C2=A0
>=C2=A0+.include=C2=A0<bsd.port.mk>=C2=A0[http://bsd.p=
ort.mk>];
>=C2=A0
>=C2=A0diff=C2=A0--git=C2=A0a/devel/cbmc/distinfo=
=C2=A0b/devel/cbmc/distinfo
>=C2=A0
>=C2=A0new=C2=A0file=C2=A0mode=
=C2=A0100644
>=C2=A0
>=C2=A0index=C2=A0000000000000..f3e6d1161c6a
>=
=C2=A0
>=C2=A0---=C2=A0/dev/null
>=C2=A0
>=C2=A0+++=C2=A0b/devel/cbmc=
/distinfo
>=C2=A0
>=C2=A0@@=C2=A0-0,0=C2=A0+1,5=C2=A0@@
>=C2=A0
>=
=C2=A0+TIMESTAMP=C2=A0=3D=C2=A01706723199
>=C2=A0
>=C2=A0+SHA256=C2=
=A0(minisat2_2.2.1.orig.tar.gz)=C2=A0=3D=C2=A0e54afa3c192c1753bc8075c0c7e12=
6d5c495d9066e3f90a2588091149ac9ca40
>=C2=A0
>=C2=A0+SIZE=C2=A0(minisat2=
_2.2.1.orig.tar.gz)=C2=A0=3D=C2=A044229
>=C2=A0
>=C2=A0+SHA256=C2=A0(di=
ffblue-cbmc-cbmc-5.95.1_GH0.tar.gz)=C2=A0=3D=C2=A0fdc1e862752430f8d069eb2f9=
c33dcd05078cf955bbc900e2cc840bcb01b3783
>=C2=A0
>=C2=A0+SIZE=C2=A0(diff=
blue-cbmc-cbmc-5.95.1_GH0.tar.gz)=C2=A0=3D=C2=A09073428
>=C2=A0
>=C2=
=A0diff=C2=A0--git=C2=A0a/devel/cbmc/files/patch-minisat-2.2.1_minisat_core=
_Solver.cc=C2=A0[http://Solver.cc]=C2=A0b/devel/cbmc/files/patch-minisat-2.=
2.1_minisat_core_Solver.cc=C2=A0[http://Solver.cc]
>=C2=A0
>=C2=A0new=
=C2=A0file=C2=A0mode=C2=A0100644
>=C2=A0
>=C2=A0index=C2=A0000000000000=
..c15c2f12fb0a
>=C2=A0
>=C2=A0---=C2=A0/dev/null
>=C2=A0
>=C2=A0+++=
=C2=A0b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc=C2=
=A0[http://Solver.cc]
>=C2=A0
>=C2=A0@@=C2=A0-0,0=C2=A0+1,20=C2=A0@@
=
>=C2=A0
>=C2=A0+---=C2=A0minisat-2.2.1/minisat/core/Solver.cc.orig=C2=
=A0[http://Solver.cc.orig]=C2=A0=C2=A0=C2=A0=C2=A02011-02-21=C2=A013:31:17=
=C2=A0UTC
>=C2=A0
>=C2=A0++++=C2=A0minisat-2.2.1/minisat/core/Solver.cc=
=C2=A0[http://Solver.cc]
>=C2=A0
>=C2=A0+@@=C2=A0-210,7=C2=A0+210,7=
=C2=A0@@=C2=A0void=C2=A0Solver::cancelUntil(int=C2=A0level)=C2=A0{
>=
=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0for=
=C2=A0(int=C2=A0c=C2=A0=3D=C2=A0trail.size()-1;=C2=A0c=C2=A0&gt;=3D=C2=
=A0trail_lim[level];=C2=A0c--){
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0Var=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0x=C2=A0=C2=A0=3D=C2=A0var(trail[c]);
>=C2=
=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0assigns=C2=A0[x]=C2=A0=3D=C2=A0l_Undef;
>=C2=A0
>=
=C2=A0+-=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0if=C2=A0(phase_saving=C2=A0>=C2=A01=C2=A0||=C2=A0(phase_saving=
=C2=A0=3D=3D=C2=A01)=C2=A0&&=C2=A0c=C2=A0>=C2=A0trail_lim.last())
>=C2=
=A0
>=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0if=C2=A0(phase_saving=C2=A0>=C2=A01=C2=A0||=C2=A0((phase_sav=
ing=C2=A0=3D=3D=C2=A01)=C2=A0&&=C2=A0c=C2=A0>=C2=A0trail_lim.last()))
>=
=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0polarity[x]=C2=A0=3D=C2=
=A0sign(trail[c]);
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0insertVarOrder(x);=C2=A0}
>=
=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0qhea=
d=C2=A0=3D=C2=A0trail_lim[level];
>=C2=A0
>=C2=A0+@@=C2=A0-666,7=C2=
=A0+666,7=C2=A0@@=C2=A0lbool=C2=A0Solver::search(int=C2=A0nof_conflicts)
=
>=C2=A0
>=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0}else{
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0//=C2=A0NO=
=C2=A0CONFLICT
>=C2=A0
>=C2=A0+-=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(nof_conflicts=C2=A0&gt;=3D=
=C2=A00=C2=A0&&=C2=A0conflictC=C2=A0&gt;=3D=C2=A0nof_conflicts=C2=A0||=
=C2=A0!withinBudget()){
>=C2=A0
>=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0((nof_conflicts=C2=
=A0&gt;=3D=C2=A00=C2=A0&&=C2=A0conflictC=C2=A0&gt;=3D=C2=A0nof_conflicts)=
=C2=A0||=C2=A0!withinBudget()){
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0//=C2=A0Reached=C2=A0bound=C2=A0on=C2=A0number=C2=A0of=C2=A0con=
flicts:
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0progress_estima=
te=C2=A0=3D=C2=A0progressEstimate();
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0cancelUntil(0);
>=C2=A0
>=C2=A0diff=C2=A0--git=C2=A0a/de=
vel/cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h=C2=A0b/devel/=
cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h
>=C2=A0
>=
=C2=A0new=C2=A0file=C2=A0mode=C2=A0100644
>=C2=A0
>=C2=A0index=C2=A0000=
000000000..fa26c6372b36
>=C2=A0
>=C2=A0---=C2=A0/dev/null
>=C2=A0
>=
=C2=A0+++=C2=A0b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTy=
pes.h
>=C2=A0
>=C2=A0@@=C2=A0-0,0=C2=A0+1,59=C2=A0@@
>=C2=A0
>=
=C2=A0+---=C2=A0minisat-2.2.1/minisat/core/SolverTypes.h.orig=C2=A0=C2=
=A0=C2=A0=C2=A02011-02-21=C2=A013:31:17=C2=A0UTC
>=C2=A0
>=C2=A0++++=
=C2=A0minisat-2.2.1/minisat/core/SolverTypes.h
>=C2=A0
>=C2=A0+@@=C2=
=A0-47,7=C2=A0+47,7=C2=A0@@=C2=A0struct=C2=A0Lit=C2=A0{
>=C2=A0
>=C2=
=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0int=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0x;
>=
=C2=A0
>=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0//=C2=A0Use=C2=A0this=C2=A0as=C2=A0a=C2=A0constructor:
>=C2=A0
>=
=C2=A0+-=C2=A0=C2=A0=C2=A0=C2=A0friend=C2=A0Lit=C2=A0mkLit(Var=C2=A0var,=
=C2=A0bool=C2=A0sign=C2=A0=3D=C2=A0false);
>=C2=A0
>=C2=A0++=C2=A0=
=C2=A0=C2=A0=C2=A0//friend=C2=A0Lit=C2=A0mkLit(Var=C2=A0var,=C2=A0bool=
=C2=A0sign=C2=A0=3D=C2=A0false);
>=C2=A0
>=C2=A0+=C2=A0
>=C2=A0
>=
=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0bool=C2=A0operator=C2=A0=3D=3D=C2=
=A0(Lit=C2=A0p)=C2=A0const=C2=A0{=C2=A0return=C2=A0x=C2=A0=3D=3D=C2=A0p.x;=
=C2=A0}
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0bool=C2=A0operato=
r=C2=A0!=3D=C2=A0(Lit=C2=A0p)=C2=A0const=C2=A0{=C2=A0return=C2=A0x=C2=A0!=
=3D=C2=A0p.x;=C2=A0}
>=C2=A0
>=C2=A0+@@=C2=A0-55,7=C2=A0+55,7=C2=A0@@=
=C2=A0struct=C2=A0Lit=C2=A0{
>=C2=A0
>=C2=A0+=C2=A0};
>=C2=A0
>=
=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+-inline=C2=
=A0=C2=A0Lit=C2=A0=C2=A0mkLit=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0(Var=C2=A0var,=
=C2=A0bool=C2=A0sign)=C2=A0{=C2=A0Lit=C2=A0p;=C2=A0p.x=C2=A0=3D=C2=A0var=
=C2=A0+=C2=A0var=C2=A0+=C2=A0(int)sign;=C2=A0return=C2=A0p;=C2=A0}
>=
=C2=A0
>=C2=A0++inline=C2=A0=C2=A0Lit=C2=A0=C2=A0mkLit=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0(Var=C2=A0var,=C2=A0bool=C2=A0sign=C2=A0=3D=C2=A0false)=
=C2=A0{=C2=A0Lit=C2=A0p;=C2=A0p.x=C2=A0=3D=C2=A0var=C2=A0+=C2=A0var=C2=
=A0+=C2=A0(int)sign;=C2=A0return=C2=A0p;=C2=A0}
>=C2=A0
>=C2=A0+=C2=
=A0inline=C2=A0=C2=A0Lit=C2=A0=C2=A0operator=C2=A0~(Lit=C2=A0p)=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0{=C2=A0Lit=C2=A0q;=C2=A0q.x=C2=A0=3D=C2=A0p.x=C2=A0^=C2=A01;=C2=A0return=
=C2=A0q;=C2=A0}
>=C2=A0
>=C2=A0+=C2=A0inline=C2=A0=C2=A0Lit=C2=A0=C2=
=A0operator=C2=A0^(Lit=C2=A0p,=C2=A0bool=C2=A0b)=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0{=C2=A0Lit=C2=A0q;=C2=A0q.x=C2=A0=3D=C2=A0p.x=C2=A0^=C2=A0(unsi=
gned=C2=A0int)b;=C2=A0return=C2=A0q;=C2=A0}
>=C2=A0
>=C2=A0+=C2=A0inlin=
e=C2=A0=C2=A0bool=C2=A0sign=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0(Lit=C2=
=A0p)=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0{=C2=A0return=C2=A0p.x=C2=A0&=C2=A01;=C2=A0}
>=C2=A0
=
>=C2=A0+@@=C2=A0-127,7=C2=A0+127,10=C2=A0@@=C2=A0class=C2=A0Clause=C2=A0{=

>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0unsigned=C2=A0has_extra=C2=A0:=C2=A01;
>=C2=A0
>=C2=A0+=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0unsigned=C2=A0reloced=C2=A0=
=C2=A0=C2=A0:=C2=A01;
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0unsigned=C2=A0size=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0:=C2=A027;=C2=A0}=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0header;
>=C2=A0
>=C2=A0++#include=C2=A0<util/pr=
agma_push.def>
>=C2=A0
>=C2=A0++#include=C2=A0<util/pragma_wzero_length=
_array.def>
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0union=C2=
=A0{=C2=A0Lit=C2=A0lit;=C2=A0float=C2=A0act;=C2=A0uint32_t=C2=A0abs;=C2=
=A0CRef=C2=A0rel;=C2=A0}=C2=A0data[0];
>=C2=A0
>=C2=A0++#include=C2=
=A0<util/pragma_pop.def>
>=C2=A0
>=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0friend=C2=A0class=C2=A0ClauseAllocator;
>=
=C2=A0
>=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+@@=C2=A0-142,11=C2=A0+145,12=
=C2=A0@@=C2=A0class=C2=A0Clause=C2=A0{
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0for=C2=A0(int=C2=A0i=C2=A0=3D=
=C2=A00;=C2=A0i=C2=A0<=C2=A0ps.size();=C2=A0i++)=C2=A0
>=C2=A0
>=C2=
=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0data[i].lit=C2=A0=3D=C2=A0ps[i];
>=C2=A0
>=C2=A0+=C2=A0
>=
=C2=A0
>=C2=A0+-=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=
=A0(header.has_extra)
>=C2=A0
>=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0if=C2=A0(header.has_extra)=C2=A0{
>=C2=A0
>=C2=
=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0if=C2=A0(header.learnt)
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0data[header.size].act=C2=A0=3D=C2=A00;
>=C2=A0
>=C2=
=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0else
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0calcAb=
straction();
>=C2=A0
>=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0}
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0}
>=C2=
=A0
>=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0//=
=C2=A0NOTE:=C2=A0This=C2=A0constructor=C2=A0cannot=C2=A0be=C2=A0used=C2=
=A0directly=C2=A0(doesn't=C2=A0allocate=C2=A0enough=C2=A0memory).
>=C2=
=A0
>=C2=A0+@@=C2=A0-157,11=C2=A0+161,12=C2=A0@@=C2=A0class=C2=A0Clause=
=C2=A0{
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0for=C2=A0(int=C2=A0i=C2=A0=3D=C2=A00;=C2=A0i=C2=A0<=C2=A0from.s=
ize();=C2=A0i++)
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0data[i].lit=C2=A0=3D=C2=A0from=
[i];
>=C2=A0
>=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+-=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(header.has_extra)
>=C2=A0
>=
=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(header.has=
_extra)=C2=A0{
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(header.learnt)
>=C2=
=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0data[header.size].act=C2=A0=3D=
=C2=A0from.data[header.size]=C2=A0[http://from.data[header.size]].act;
>=
=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0else=C2=A0
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0data[header.size].abs=C2=A0=3D=C2=A0from.data[header.size]=
=C2=A0[http://from.data[header.size]].abs;
>=C2=A0
>=C2=A0++=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0}
>=C2=A0
>=C2=A0+=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0}
>=C2=A0
>=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+=
=C2=A0public:
>=C2=A0
>=C2=A0diff=C2=A0--git=C2=A0a/devel/cbmc/files/pa=
tch-minisat-2.2.1_minisat_mtl_IntTypes.h=C2=A0b/devel/cbmc/files/patch-mini=
sat-2.2.1_minisat_mtl_IntTypes.h
>=C2=A0
>=C2=A0new=C2=A0file=C2=A0mode=
=C2=A0100644
>=C2=A0
>=C2=A0index=C2=A0000000000000..d8c9ddedb701
>=
=C2=A0
>=C2=A0---=C2=A0/dev/null
>=C2=A0
>=C2=A0+++=C2=A0b/devel/cbmc=
/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h
>=C2=A0
>=C2=A0@@=
=C2=A0-0,0=C2=A0+1,12=C2=A0@@
>=C2=A0
>=C2=A0+---=C2=A0minisat-2.2.1/mi=
nisat/mtl/IntTypes.h.orig=C2=A0=C2=A0=C2=A0=C2=A02011-02-21=C2=A013:31:17=
=C2=A0UTC
>=C2=A0
>=C2=A0++++=C2=A0minisat-2.2.1/minisat/mtl/IntTypes.h=

>=C2=A0
>=C2=A0+@@=C2=A0-31,7=C2=A0+31,9=C2=A0@@=C2=A0OF=C2=A0OR=C2=
=A0IN=C2=A0CONNECTION=C2=A0WITH=C2=A0THE=C2=A0SOFTWARE=C2=A0OR=C2=A0THE=
=C2=A0USE=C2=A0OR=C2=A0OT
>=C2=A0
>=C2=A0+=C2=A0#else
>=C2=A0
>=
=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+=C2=A0#=C2=A0=C2=A0=C2=A0include=C2=A0<st=
dint.h>
>=C2=A0
>=C2=A0++#ifndef=C2=A0_MSC_VER
>=C2=A0
>=C2=A0+=
=C2=A0#=C2=A0=C2=A0=C2=A0include=C2=A0<inttypes.h>
>=C2=A0
>=C2=A0++#en=
dif
>=C2=A0
>=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+=C2=A0The=C2=A0branch=
=C2=A0main=C2=A0has=C2=A0been=C2=A0updated=C2=A0by=C2=A0olivier:
>=C2=
=A0
>=C2=A0URL:=C2=A0https://cgit.FreeBSD.org/ports/commit/?id=3D7f087b72=
0e52d51b22db0da2d7565418a0e428ef
>=C2=A0
>=C2=A0commit=C2=A07f087b720e5=
2d51b22db0da2d7565418a0e428ef
>=C2=A0
>=C2=A0Author:=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0Olivier=C2=A0Cochard=C2=A0<olivier@FreeBSD.org>
>=C2=A0
=
>=C2=A0AuthorDate:=C2=A02024-02-01=C2=A017:50:02=C2=A0+0000
>=C2=A0
>=
=C2=A0Commit:=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0Olivier=C2=A0Cochard=C2=A0<olivi=
er@FreeBSD.org>
>=C2=A0
>=C2=A0CommitDate:=C2=A02024-02-01=C2=A017:53:5=
5=C2=A0+0000
>=C2=A0
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0devel/cbmc:=C2=
=A0add=C2=A0new=C2=A0port
>=C2=A0
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0
>=
=C2=A0
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0Bounded=C2=A0Model=C2=A0Checker=
=C2=A0for=C2=A0C=C2=A0and=C2=A0C++=C2=A0programs
>=C2=A0
>=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0https://github.com/diffblue/cbmc
>=C2=A0
>=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0
>=C2=A0
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0Spon=
sored=C2=A0by:=C2=A0=C2=A0=C2=A0Netflix
>=C2=A0
>=C2=A0---
>=C2=A0
=
>=C2=A0=C2=A0devel/Makefile=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A0=C2=A01=C2=A0+
>=C2=A0
>=C2=
=A0=C2=A0devel/cbmc/Makefile=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0|=C2=A046=C2=A0+++++++++++++++++
>=C2=A0
>=C2=A0=C2=A0devel/cbmc/=
distinfo=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A0=C2=A05=
=C2=A0++
>=C2=A0
>=C2=A0=C2=A0.../patch-minisat-2.2.1_minisat_core_Solv=
er.cc=C2=A0[http://Solver.cc]=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A020=C2=
=A0++++++++
>=C2=A0
>=C2=A0=C2=A0.../patch-minisat-2.2.1_minisat_core_S=
olverTypes.h=C2=A0|=C2=A059=C2=A0++++++++++++++++++++++
>=C2=A0
>=C2=
=A0=C2=A0.../patch-minisat-2.2.1_minisat_mtl_IntTypes.h=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0|=C2=A012=C2=A0+++++
>=C2=A0
>=C2=A0=C2=A0.../files/patc=
h-minisat-2.2.1_minisat_mtl_Vec.h=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A016=C2=A0+++=
+++
>=C2=A0
>=C2=A0=C2=A0.../files/patch-minisat-2.2.1_minisat_mtl_XAll=
oc.h=C2=A0|=C2=A019=C2=A0+++++++
>=C2=A0
>=C2=A0=C2=A0.../patch-minisat=
-2.2.1_minisat_simp_SimpSolver.cc=C2=A0[http://SimpSolver.cc]=C2=A0|=C2=
=A037=C2=A0++++++++++++++
>=C2=A0
>=C2=A0=C2=A0.../patch-minisat-2.2.1_=
minisat_utils_Options.cc=C2=A0[http://Options.cc]=C2=A0=C2=A0=C2=A0|=C2=
=A015=C2=A0++++++
>=C2=A0
>=C2=A0=C2=A0.../patch-minisat-2.2.1_minisat_=
utils_Options.h=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A030=C2=A0+++++++++++
>=C2=
=A0
>=C2=A0=C2=A0.../patch-minisat-2.2.1_minisat_utils_ParseUtils.h=C2=
=A0|=C2=A033=C2=A0++++++++++++
>=C2=A0
>=C2=A0=C2=A0.../patch-minisat-2=
.2.1_minisat_utils_System.h=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A011=C2=A0+++=
+
>=C2=A0
>=C2=A0=C2=A0devel/cbmc/files/patch-src_common=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A011=C2=A0++++
>=C2=A0
>=C2=A0=C2=A0.../fi=
les/patch-src_solvers_sat_external__sat.cpp=C2=A0=C2=A0|=C2=A013=C2=A0+++++=

>=C2=A0
>=C2=A0=C2=A0devel/cbmc/files/patch-src_util_optional.h=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A029=C2=A0+++++++++=
++
>=C2=A0
>=C2=A0=C2=A0devel/cbmc/pkg-descr=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0|=C2=A0=C2=A07=C2=A0+++
>=C2=A0
>=C2=A0=C2=A0devel/cb=
mc/pkg-plist=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A023=C2=A0++++++=
+++
>=C2=A0
>=C2=A0=C2=A018=C2=A0files=C2=A0changed,=C2=A0387=C2=A0inse=
rtions(+)
>=C2=A0
>=C2=A0diff=C2=A0--git=C2=A0a/devel/Makefile=C2=A0b/d=
evel/Makefile
>=C2=A0
>=C2=A0index=C2=A04da71e0953a1..51481c8a3aca=
=C2=A0100644
>=C2=A0
>=C2=A0---=C2=A0a/devel/Makefile
>=C2=A0
>=
=C2=A0+++=C2=A0b/devel/Makefile
>=C2=A0
>=C2=A0@@=C2=A0-351,6=C2=A0+351=
,7=C2=A0@@
>=C2=A0
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=C2=A0+=
=3D=C2=A0catch2
>=C2=A0
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=
=C2=A0+=3D=C2=A0cbang
>=C2=A0
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBD=
IR=C2=A0+=3D=C2=A0cbfmt
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=
=C2=A0+=3D=C2=A0cbmc
>=C2=A0
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDI=
R=C2=A0+=3D=C2=A0cbrowser
>=C2=A0
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0SUBDIR=C2=A0+=3D=C2=A0cc65
>=C2=A0
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0SUBDIR=C2=A0+=3D=C2=A0ccache
>=C2=A0
>=C2=A0diff=C2=A0--git=
=C2=A0a/devel/cbmc/Makefile=C2=A0b/devel/cbmc/Makefile
>=C2=A0
>=C2=
=A0new=C2=A0file=C2=A0mode=C2=A0100644
>=C2=A0
>=C2=A0index=C2=A0000000=
000000..c7f7b3650e63
>=C2=A0
>=C2=A0---=C2=A0/dev/null
>=C2=A0
>=
=C2=A0+++=C2=A0b/devel/cbmc/Makefile
>=C2=A0
>=C2=A0@@=C2=A0-0,0=C2=
=A0+1,46=C2=A0@@
>=C2=A0
>=C2=A0+PORTNAME=3D=C2=A0=C2=A0=C2=A0=C2=A0cbm=
c
>=C2=A0
>=C2=A0+PORTVERSION=3D=C2=A0=C2=A0=C2=A0=C2=A05.95.1
>=
=C2=A0
>=C2=A0+DISTVERSIONPREFIX=3D=C2=A0=C2=A0=C2=A0=C2=A0cbmc-
>=
=C2=A0
>=C2=A0+CATEGORIES=3D=C2=A0=C2=A0=C2=A0=C2=A0devel
>=C2=A0
>=
=C2=A0+MASTER_SITES=3D=C2=A0=C2=A0=C2=A0=C2=A0DEBIAN/pool/main/m/minisat2:m=
inisat
>=C2=A0
>=C2=A0+DISTFILES=3D=C2=A0=C2=A0=C2=A0=C2=A0minisat2_2.2=
.1.orig.tar.gz:minisat
>=C2=A0
>=C2=A0+
>=C2=A0
>=C2=A0+MAINTAINER=
=3D=C2=A0=C2=A0=C2=A0=C2=A0olivier@FreeBSD.org
>=C2=A0
>=C2=A0+COMMENT=
=3D=C2=A0=C2=A0=C2=A0=C2=A0Bounded=C2=A0Model=C2=A0Checker=C2=A0for=C2=
=A0C=C2=A0and=C2=A0C++=C2=A0programs
>=C2=A0
>=C2=A0+WWW=3D=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0https://github.com/diffblue/cbmc
>=
=C2=A0
>=C2=A0+
>=C2=A0
>=C2=A0+LICENSE=3D=C2=A0=C2=A0=C2=A0=C2=A0BSD=
4CLAUSE
>=C2=A0
>=C2=A0+LICENSE_FILE=3D=C2=A0=C2=A0=C2=A0=C2=A0${WRKSRC=
}/LICENSE
>=C2=A0
>=C2=A0+
>=C2=A0
>=C2=A0+BUILD_DEPENDS=3D=C2=
=A0=C2=A0=C2=A0=C2=A0${LOCALBASE}/bin/flex:textproc/flex
>=C2=A0
>=
=C2=A0+RUN_DEPENDS=3D=C2=A0=C2=A0=C2=A0=C2=A0${LOCALBASE}/bin/cvc5:math/cvc=
5=C2=A0\
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0${LOCALBASE}/bin/z3:math/z3
>=C2=A0
>=C2=A0+
>=C2=A0
>=C2=
=A0+USES=3D=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0gmake=C2=A0bison=
=C2=A0python=C2=A0shebangfix
>=C2=A0
>=C2=A0+
>=C2=A0
>=C2=A0+USE_G=
ITHUB=3D=C2=A0=C2=A0=C2=A0=C2=A0yes
>=C2=A0
>=C2=A0+GH_ACCOUNT=3D=C2=
=A0=C2=A0=C2=A0=C2=A0diffblue
>=C2=A0
>=C2=A0+SHEBANG_FILES=3D=C2=A0=
=C2=A0=C2=A0=C2=A0${WRKSRC}/scripts/ls_parse.py=C2=A0[http://parse.py]
>=
=C2=A0
>=C2=A0+WRKSRC_minisat=3D=C2=A0=C2=A0=C2=A0=C2=A0${WRKDIR}/minisat=
2-2.2.1
>=C2=A0
>=C2=A0+
>=C2=A0
>=C2=A0+post-patch:
>=C2=A0
>=
=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0@${REINPLACE_CMD}=C2=A0-e=C2=A0's|.*git=
=C2=A0describe=C2=A0--tags.*|GIT_INFO=C2=A0=3D=C2=A0${PORTNAME}-${PORTVERSI=
ON}|'=C2=A0\
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0${WRKSRC}/src/util/Makefile
>=C2=A0
>=C2=A0+post-extract:
>=
=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0@${MV}=C2=A0${WRKSRC_minisat}=
=C2=A0${WRKSRC}/minisat-2.2.1
>=C2=A0
>=C2=A0+
>=C2=A0
>=C2=A0+do-b=
uild:
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0@${MKDIR}=C2=A0${STAGEDIR=
}
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0cd=C2=A0${WRKSRC}=C2=A0&&=
=C2=A0${GMAKE}=C2=A0-C=C2=A0src=C2=A0-j${MAKE_JOBS_NUMBER}
>=C2=A0
>=
=C2=A0+
>=C2=A0
>=C2=A0+do-install:
>=C2=A0
>=C2=A0+.=C2=A0=C2=
=A0for=C2=A0x=C2=A0in=C2=A0cbmc=C2=A0crangler=C2=A0goto-analyzer=C2=A0goto-=
cc=C2=A0goto-diff=C2=A0goto-instrument=C2=A0\
>=C2=A0
>=C2=A0+=C2=A0=
=C2=A0=C2=A0=C2=A0goto-inspect=C2=A0goto-harness=C2=A0goto-synthesizer=
=C2=A0symtab2gb
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${INSTALL_PROGR=
AM}=C2=A0${WRKSRC}/src/${x}/${x}=C2=A0${STAGEDIR}${PREFIX}/bin/
>=C2=
=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${INSTALL_MAN}=C2=A0${WRKSRC}/doc/man=
/${x}.1=C2=A0${STAGEDIR}${PREFIX}/share/man/man1/
>=C2=A0
>=C2=A0+.=
=C2=A0=C2=A0endfor
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${LN}=C2=
=A0-sf=C2=A0goto-cc=C2=A0${STAGEDIR}${PREFIX}/bin/goto-gcc
>=C2=A0
>=
=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${LN}=C2=A0-sf=C2=A0goto-cc=C2=A0${STAGEDIR}=
${PREFIX}/bin/goto-ld
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${INSTALL=
_SCRIPT}=C2=A0${WRKSRC}/scripts/ls_parse.py=C2=A0[http://parse.py]=C2=A0${S=
TAGEDIR}${PREFIX}/bin/
>=C2=A0
>=C2=A0+
>=C2=A0
>=C2=A0+.include=
=C2=A0<bsd.port.mk>=C2=A0[http://bsd.port.mk>];
>=C2=A0
>=C2=A0diff=
=C2=A0--git=C2=A0a/devel/cbmc/distinfo=C2=A0b/devel/cbmc/distinfo
>=C2=
=A0
>=C2=A0new=C2=A0file=C2=A0mode=C2=A0100644
>=C2=A0
>=C2=A0index=
=C2=A0000000000000..f3e6d1161c6a
>=C2=A0
>=C2=A0---=C2=A0/dev/null
>=
=C2=A0
>=C2=A0+++=C2=A0b/devel/cbmc/distinfo
>=C2=A0
>=C2=A0@@=C2=
=A0-0,0=C2=A0+1,5=C2=A0@@
>=C2=A0
>=C2=A0+TIMESTAMP=C2=A0=3D=C2=A017067=
23199
>=C2=A0
>=C2=A0+SHA256=C2=A0(minisat2_2.2.1.orig.tar.gz)=C2=A0=3D=
=C2=A0e54afa3c192c1753bc8075c0c7e126d5c495d9066e3f90a2588091149ac9ca40
>=
=C2=A0
>=C2=A0+SIZE=C2=A0(minisat2_2.2.1.orig.tar.gz)=C2=A0=3D=C2=A044229=

>=C2=A0
>=C2=A0+SHA256=C2=A0(diffblue-cbmc-cbmc-5.95.1_GH0.tar.gz)=
=C2=A0=3D=C2=A0fdc1e862752430f8d069eb2f9c33dcd05078cf955bbc900e2cc840bcb01b=
3783
>=C2=A0
>=C2=A0+SIZE=C2=A0(diffblue-cbmc-cbmc-5.95.1_GH0.tar.gz)=
=C2=A0=3D=C2=A09073428
>=C2=A0
>=C2=A0diff=C2=A0--git=C2=A0a/devel/cbmc=
/files/patch-minisat-2.2.1_minisat_core_Solver.cc=C2=A0[http://Solver.cc]=
=C2=A0b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc=C2=
=A0[http://Solver.cc]
>=C2=A0
>=C2=A0new=C2=A0file=C2=A0mode=C2=A010064=
4
>=C2=A0
>=C2=A0index=C2=A0000000000000..c15c2f12fb0a
>=C2=A0
>=
=C2=A0---=C2=A0/dev/null
>=C2=A0
>=C2=A0+++=C2=A0b/devel/cbmc/files/pat=
ch-minisat-2.2.1_minisat_core_Solver.cc=C2=A0[http://Solver.cc]
>=C2=
=A0
>=C2=A0@@=C2=A0-0,0=C2=A0+1,20=C2=A0@@
>=C2=A0
>=C2=A0+---=C2=
=A0minisat-2.2.1/minisat/core/Solver.cc.orig=C2=A0[http://Solver.cc.orig]=
=C2=A0=C2=A0=C2=A0=C2=A02011-02-21=C2=A013:31:17=C2=A0UTC
>=C2=A0
>=
=C2=A0++++=C2=A0minisat-2.2.1/minisat/core/Solver.cc=C2=A0[http://Solver.cc=
]
>=C2=A0
>=C2=A0+@@=C2=A0-210,7=C2=A0+210,7=C2=A0@@=C2=A0void=C2=A0Sol=
ver::cancelUntil(int=C2=A0level)=C2=A0{
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0for=C2=A0(int=C2=A0c=C2=A0=3D=
=C2=A0trail.size()-1;=C2=A0c=C2=A0&gt;=3D=C2=A0trail_lim[level];=C2=A0c--){=

>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0Var=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0x=C2=
=A0=C2=A0=3D=C2=A0var(trail[c]);
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0assigns=C2=
=A0[x]=C2=A0=3D=C2=A0l_Undef;
>=C2=A0
>=C2=A0+-=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(phase_saving=
=C2=A0>=C2=A01=C2=A0||=C2=A0(phase_saving=C2=A0=3D=3D=C2=A01)=C2=A0&&=C2=
=A0c=C2=A0>=C2=A0trail_lim.last())
>=C2=A0
>=C2=A0++=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(phase_sav=
ing=C2=A0>=C2=A01=C2=A0||=C2=A0((phase_saving=C2=A0=3D=3D=C2=A01)=C2=A0&&=
=C2=A0c=C2=A0>=C2=A0trail_lim.last()))
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0polarity[x]=C2=A0=3D=C2=A0sign(trail[c]);
>=C2=A0
>=
=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0insertVarOrder(x);=C2=A0}
>=C2=A0
>=C2=A0+=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0qhead=C2=A0=3D=C2=A0trail_lim[=
level];
>=C2=A0
>=C2=A0+@@=C2=A0-666,7=C2=A0+666,7=C2=A0@@=C2=A0lbool=
=C2=A0Solver::search(int=C2=A0nof_conflicts)
>=C2=A0
>=C2=A0+=C2=A0
>=
=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0}els=
e{
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0//=C2=A0NO=C2=A0CONFLICT
>=C2=A0
>=C2=
=A0+-=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0if=C2=A0(nof_conflicts=C2=A0&gt;=3D=C2=A00=C2=A0&&=C2=A0conflictC=
=C2=A0&gt;=3D=C2=A0nof_conflicts=C2=A0||=C2=A0!withinBudget()){
>=C2=
=A0
>=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0if=C2=A0((nof_conflicts=C2=A0&gt;=3D=C2=A00=C2=A0&&=C2=A0con=
flictC=C2=A0&gt;=3D=C2=A0nof_conflicts)=C2=A0||=C2=A0!withinBudget()){
>=
=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0//=C2=A0Reached=C2=A0bound=
=C2=A0on=C2=A0number=C2=A0of=C2=A0conflicts:
>=C2=A0
>=C2=A0+=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0progress_estimate=C2=A0=3D=C2=A0progressEstimate();=

>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0cancelUntil(0);
>=
=C2=A0
>=C2=A0diff=C2=A0--git=C2=A0a/devel/cbmc/files/patch-minisat-2.2.1=
_minisat_core_SolverTypes.h=C2=A0b/devel/cbmc/files/patch-minisat-2.2.1_min=
isat_core_SolverTypes.h
>=C2=A0
>=C2=A0new=C2=A0file=C2=A0mode=C2=A0100=
644
>=C2=A0
>=C2=A0index=C2=A0000000000000..fa26c6372b36
>=C2=A0
>=
=C2=A0---=C2=A0/dev/null
>=C2=A0
>=C2=A0+++=C2=A0b/devel/cbmc/files/pat=
ch-minisat-2.2.1_minisat_core_SolverTypes.h
>=C2=A0
>=C2=A0@@=C2=A0-0,0=
=C2=A0+1,59=C2=A0@@
>=C2=A0
>=C2=A0+---=C2=A0minisat-2.2.1/minisat/core=
/SolverTypes.h.orig=C2=A0=C2=A0=C2=A0=C2=A02011-02-21=C2=A013:31:17=C2=
=A0UTC
>=C2=A0
>=C2=A0++++=C2=A0minisat-2.2.1/minisat/core/SolverTypes.=
h
>=C2=A0
>=C2=A0+@@=C2=A0-47,7=C2=A0+47,7=C2=A0@@=C2=A0struct=C2=A0Lit=
=C2=A0{
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0int=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0x;
>=C2=A0
>=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0//=C2=A0Use=C2=A0this=C2=A0as=C2=A0a=C2=A0con=
structor:
>=C2=A0
>=C2=A0+-=C2=A0=C2=A0=C2=A0=C2=A0friend=C2=A0Lit=
=C2=A0mkLit(Var=C2=A0var,=C2=A0bool=C2=A0sign=C2=A0=3D=C2=A0false);
>=
=C2=A0
>=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0//friend=C2=A0Lit=C2=A0mkLit(Var=
=C2=A0var,=C2=A0bool=C2=A0sign=C2=A0=3D=C2=A0false);
>=C2=A0
>=C2=A0+=
=C2=A0
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0bool=C2=A0operator=
=C2=A0=3D=3D=C2=A0(Lit=C2=A0p)=C2=A0const=C2=A0{=C2=A0return=C2=A0x=C2=
=A0=3D=3D=C2=A0p.x;=C2=A0}
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0bool=C2=A0operator=C2=A0!=3D=C2=A0(Lit=C2=A0p)=C2=A0const=C2=A0{=
=C2=A0return=C2=A0x=C2=A0!=3D=C2=A0p.x;=C2=A0}
>=C2=A0
>=C2=A0+@@=C2=
=A0-55,7=C2=A0+55,7=C2=A0@@=C2=A0struct=C2=A0Lit=C2=A0{
>=C2=A0
>=C2=
=A0+=C2=A0};
>=C2=A0
>=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+=C2=A0
>=
=C2=A0
>=C2=A0+-inline=C2=A0=C2=A0Lit=C2=A0=C2=A0mkLit=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0(Var=C2=A0var,=C2=A0bool=C2=A0sign)=C2=A0{=C2=A0Lit=C2=A0p;=
=C2=A0p.x=C2=A0=3D=C2=A0var=C2=A0+=C2=A0var=C2=A0+=C2=A0(int)sign;=C2=A0ret=
urn=C2=A0p;=C2=A0}
>=C2=A0
>=C2=A0++inline=C2=A0=C2=A0Lit=C2=A0=C2=
=A0mkLit=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0(Var=C2=A0var,=C2=A0bool=C2=A0sign=
=C2=A0=3D=C2=A0false)=C2=A0{=C2=A0Lit=C2=A0p;=C2=A0p.x=C2=A0=3D=C2=A0var=
=C2=A0+=C2=A0var=C2=A0+=C2=A0(int)sign;=C2=A0return=C2=A0p;=C2=A0}
>=
=C2=A0
>=C2=A0+=C2=A0inline=C2=A0=C2=A0Lit=C2=A0=C2=A0operator=C2=A0~(Lit=
=C2=A0p)=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0{=C2=A0Lit=C2=A0q;=C2=A0q.x=C2=A0=3D=C2=A0p.x=C2=A0^=
=C2=A01;=C2=A0return=C2=A0q;=C2=A0}
>=C2=A0
>=C2=A0+=C2=A0inline=C2=
=A0=C2=A0Lit=C2=A0=C2=A0operator=C2=A0^(Lit=C2=A0p,=C2=A0bool=C2=A0b)=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0{=C2=A0Lit=C2=A0q;=C2=A0q.x=C2=A0=3D=C2=
=A0p.x=C2=A0^=C2=A0(unsigned=C2=A0int)b;=C2=A0return=C2=A0q;=C2=A0}
>=
=C2=A0
>=C2=A0+=C2=A0inline=C2=A0=C2=A0bool=C2=A0sign=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0(Lit=C2=A0p)=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0{=C2=A0return=C2=A0p.x=C2=
=A0&=C2=A01;=C2=A0}
>=C2=A0
>=C2=A0+@@=C2=A0-127,7=C2=A0+127,10=C2=
=A0@@=C2=A0class=C2=A0Clause=C2=A0{
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0unsigned=C2=A0has_extra=C2=A0:=C2=
=A01;
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0unsigned=C2=A0reloced=C2=A0=C2=A0=C2=A0:=C2=A01;
>=C2=A0
>=
=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0unsigned=C2=
=A0size=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0:=C2=A027;=C2=A0}=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0header;
>=
=C2=A0
>=C2=A0++#include=C2=A0<util/pragma_push.def>
>=C2=A0
>=C2=
=A0++#include=C2=A0<util/pragma_wzero_length_array.def>
>=C2=A0
>=C2=
=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0union=C2=A0{=C2=A0Lit=C2=A0lit;=C2=A0floa=
t=C2=A0act;=C2=A0uint32_t=C2=A0abs;=C2=A0CRef=C2=A0rel;=C2=A0}=C2=A0data[0]=
;
>=C2=A0
>=C2=A0++#include=C2=A0<util/pragma_pop.def>
>=C2=A0
>=
=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0friend=
=C2=A0class=C2=A0ClauseAllocator;
>=C2=A0
>=C2=A0+=C2=A0
>=C2=A0
>=
=C2=A0+@@=C2=A0-142,11=C2=A0+145,12=C2=A0@@=C2=A0class=C2=A0Clause=C2=A0{=

>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0for=C2=A0(int=C2=A0i=C2=A0=3D=C2=A00;=C2=A0i=C2=A0<=C2=A0ps.size();=
=C2=A0i++)=C2=A0
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0data[i].lit=C2=A0=3D=C2=A0ps[i=
];
>=C2=A0
>=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+-=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(header.has_extra)
>=C2=A0
>=C2=
=A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(header.has_ex=
tra)=C2=A0{
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(header.learnt)
>=C2=A0
=
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0data[header.size].act=C2=A0=3D=C2=
=A00;
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0else
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0calcAbstraction();
>=C2=A0
>=C2=A0++=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0}
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0}
>=C2=A0
>=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0//=C2=A0NOTE:=C2=A0This=C2=A0constructor=C2=
=A0cannot=C2=A0be=C2=A0used=C2=A0directly=C2=A0(doesn't=C2=A0allocate=C2=
=A0enough=C2=A0memory).
>=C2=A0
>=C2=A0+@@=C2=A0-157,11=C2=A0+161,12=
=C2=A0@@=C2=A0class=C2=A0Clause=C2=A0{
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0for=C2=A0(int=C2=A0i=C2=A0=3D=
=C2=A00;=C2=A0i=C2=A0<=C2=A0from.size();=C2=A0i++)
>=C2=A0
>=C2=A0+=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0data[i].lit=C2=A0=3D=C2=A0from[i];
>=C2=A0
>=C2=A0+=C2=A0
>=
=C2=A0
>=C2=A0+-=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=
=A0(header.has_extra)
>=C2=A0
>=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0if=C2=A0(header.has_extra)=C2=A0{
>=C2=A0
>=C2=
=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0if=C2=A0(header.learnt)
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0data[header.size].act=C2=A0=3D=C2=A0from.data[header.size]=
=C2=A0[http://from.data[header.size]].act;
>=C2=A0
>=C2=A0+=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0else=
=C2=A0
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0data[header.size].=
abs=C2=A0=3D=C2=A0from.data[header.size]=C2=A0[http://from.data[header.size=
]].abs;
>=C2=A0
>=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0}
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0}
>=C2=A0
>=
=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+=C2=A0public:
>=C2=A0
>=C2=A0diff=
=C2=A0--git=C2=A0a/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntType=
s.h=C2=A0b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h
>=
=C2=A0
>=C2=A0new=C2=A0file=C2=A0mode=C2=A0100644
>=C2=A0
>=C2=A0inde=
x=C2=A0000000000000..d8c9ddedb701
>=C2=A0
>=C2=A0---=C2=A0/dev/null
>=
=C2=A0
>=C2=A0+++=C2=A0b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl=
_IntTypes.h
>=C2=A0
>=C2=A0@@=C2=A0-0,0=C2=A0+1,12=C2=A0@@
>=C2=A0
=
>=C2=A0+---=C2=A0minisat-2.2.1/minisat/mtl/IntTypes.h.orig=C2=A0=C2=A0=
=C2=A0=C2=A02011-02-21=C2=A013:31:17=C2=A0UTC
>=C2=A0
>=C2=A0++++=C2=
=A0minisat-2.2.1/minisat/mtl/IntTypes.h
>=C2=A0
>=C2=A0+@@=C2=A0-31,7=
=C2=A0+31,9=C2=A0@@=C2=A0OF=C2=A0OR=C2=A0IN=C2=A0CONNECTION=C2=A0WITH=C2=
=A0THE=C2=A0SOFTWARE=C2=A0OR=C2=A0THE=C2=A0USE=C2=A0OR=C2=A0OT
>=C2=A0
=
>=C2=A0+=C2=A0#else
>=C2=A0
>=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+=C2=
=A0#=C2=A0=C2=A0=C2=A0include=C2=A0<stdint.h>
>=C2=A0
>=C2=A0++#ifndef=
=C2=A0_MSC_VER
>=C2=A0
>=C2=A0+=C2=A0#=C2=A0=C2=A0=C2=A0include=C2=
=A0<inttypes.h>
>=C2=A0
>=C2=A0++#endif
>=C2=A0
>=C2=A0+=C2=A0
>=
=C2=A0
>=C2=A0+=C2=A0#endiffile=C2=A0mode=C2=A0100644
>=C2=A0
>=C2=
=A0index=C2=A0000000000000..f0dd61cd9963
>=C2=A0
>=C2=A0---=C2=A0/dev/n=
ull
>=C2=A0
>=C2=A0+++=C2=A0b/devel/cbmc/files/patch-src_solvers_sat_ex=
ternal__sat.cpp
>=C2=A0
>=C2=A0@@=C2=A0-0,0=C2=A0+1,13=C2=A0@@
>=
=C2=A0
>=C2=A0+---=C2=A0src/solvers/sat/external_sat.cpp.orig=C2=A0=C2=
=A0=C2=A0=C2=A02023-10-30=C2=A012:11:18=C2=A0UTC
>=C2=A0
>=C2=A0++++=
=C2=A0src/solvers/sat/external_sat.cpp
>=C2=A0
>=C2=A0+@@=C2=A0-119,8=
=C2=A0+119,8=C2=A0@@=C2=A0external_satt::resultt=C2=A0external_satt::parse_=
result(std
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0{
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0try
>=C2=A0
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0{
>=C2=A0
>=C2=A0+-=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0signed=C2=A0long=C2=A0long=C2=A0as_long=C2=A0=3D=
=C2=A0std::stol(assignment_string);
>=C2=A0
>=C2=A0+-=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0size_t=C2=A0index=C2=A0=3D=
=C2=A0std::labs(as_long);
>=C2=A0
>=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0signed=C2=A0long=C2=A0long=C2=A0as_long=
=C2=A0=3D=C2=A0std::stoll(assignment_string);
>=C2=A0
>=C2=A0++=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0size_t=C2=A0index=
=C2=A0=3D=C2=A0std::llabs(as_long);
>=C2=A0
>=C2=A0+=C2=A0
>=C2=A0
=
>=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0if(index=C2=A0&gt;=3D=C2=A0number_of_variables)
>=C2=A0
>=C2=A0+=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0{
>=
=C2=A0
>=C2=A0diff=C2=A0--git=C2=A0a/devel/cbmc/files/patch-src_util_opti=
onal.h=C2=A0b/devel/cbmc/files/patch-src_util_optional.h
>=C2=A0
>=
=C2=A0new=C2=A0file=C2=A0mode=C2=A0100644
>=C2=A0
>=C2=A0index=C2=A0000=
000000000..4507ce0ade2b
>=C2=A0
>=C2=A0---=C2=A0/dev/null
>=C2=A0
>=
=C2=A0+++=C2=A0b/devel/cbmc/files/patch-src_util_optional.h
>=C2=A0
>=
=C2=A0@@=C2=A0-0,0=C2=A0+1,29=C2=A0@@
>=C2=A0
>=C2=A0+---=C2=A0src/util=
/optional.h.orig=C2=A0=C2=A0=C2=A0=C2=A02023-10-30=C2=A012:11:18=C2=A0UTC=

>=C2=A0
>=C2=A0++++=C2=A0src/util/optional.h
>=C2=A0
>=C2=A0+@@=
=C2=A0-11,20=C2=A0+11,20=C2=A0@@=C2=A0Author:=C2=A0Diffblue=C2=A0Ltd.
>=
=C2=A0
>=C2=A0+=C2=A0#define=C2=A0CPROVER_UTIL_OPTIONAL_H
>=C2=A0
>=
=C2=A0+=C2=A0
>=C2=A0
>=C2=A0+=C2=A0#if=C2=A0defined=C2=A0__clang__
>=
=C2=A0
>=C2=A0+-=C2=A0=C2=A0#pragma=C2=A0clang=C2=A0diagnostic=C2=A0push=
=C2=A0ignore=C2=A0"-Wall"
>=C2=A0
>=C2=A0+-=C2=A0=C2=A0#pragma=C2=A0cla=
ng=C2=A0diagnostic=C2=A0push=C2=A0ignore=C2=A0"-Wpedantic"
>=C2=A0
>=
=C2=A0++=C2=A0=C2=A0#pragma=C2=A0clang=C2=A0diagnostic=C2=A0push
>=C2=
=A0
>=C2=A0++=C2=A0=C2=A0#pragma=C2=A0clang=C2=A0diagnostic=C2=A0ignored=
=C2=A0"-Wall"
>=C2=A0
>=C2=A0++=C2=A0=C2=A0#pragma=C2=A0clang=C2=A0diag=
nostic=C2=A0ignored=C2=A0"-Wpedantic"
>=C2=A0
>=C2=A0+=C2=A0#elif=C2=
=A0defined=C2=A0__GNUC__
>=C2=A0
>=C2=A0+-=C2=A0=C2=A0#pragma=C2=A0GCC=
=C2=A0diagnostic=C2=A0push=C2=A0ignore=C2=A0"-Wall"
>=C2=A0
>=C2=A0+-=
=C2=A0=C2=A0#pragma=C2=A0GCC=C2=A0diagnostic=C2=A0push=C2=A0ignore=C2=A0"-W=
pedantic"
>=C2=A0
>=C2=A0++=C2=A0=C2=A0#pragma=C2=A0GCC=C2=A0diagnostic=
=C2=A0push
>=C2=A0
>=C2=A0++=C2=A0=C2=A0#pragma=C2=A0GCC=C2=A0diagnosti=
c=C2=A0ignored=C2=A0"-Wall"
>=C2=A0
>=C2=A0++=C2=A0=C2=A0#pragma=C2=
=A0GCC=C2=A0diagnostic=C2=A0ignored=C2=A0"-Wpedantic"
>=C2=A0
>=C2=
=A0+=C2=A0#elif=C2=A0defined=C2=A0_MSC_VER
>=C2=A0
>=C2=A0+=C2=A0=C2=
=A0=C2=A0#pragma=C2=A0warning(push)
>=C2=A0
>=C2=A0+=C2=A0#endif
>=
=C2=A0
>=C2=A0+=C2=A0#include=C2=A0<nonstd/optional.hpp>
>=C2=A0
>=
=C2=A0+=C2=A0#if=C2=A0defined=C2=A0=C2=A0__clang__
>=C2=A0
>=C2=A0+=
=C2=A0=C2=A0=C2=A0#pragma=C2=A0clang=C2=A0diagnostic=C2=A0pop
>=C2=A0
>=
=C2=A0+-=C2=A0=C2=A0#pragma=C2=A0clang=C2=A0diagnostic=C2=A0pop
>=C2=
=A0
>=C2=A0+=C2=A0#elif=C2=A0defined=C2=A0=C2=A0__GNUC__
>=C2=A0
>=
=C2=A0+-=C2=A0=C2=A0#pragma=C2=A0GCC=C2=A0diagnostic=C2=A0pop
>=C2=A0
>=
=C2=A0+=C2=A0=C2=A0=C2=A0#pragma=C2=A0GCC=C2=A0diagnostic=C2=A0pop
>=
=C2=A0
>=C2=A0+=C2=A0#elif=C2=A0defined=C2=A0_MSC_VER
>=C2=A0
>=C2=
=A0+=C2=A0=C2=A0=C2=A0#pragma=C2=A0warning(pop)
>=C2=A0
>=C2=A0diff=
=C2=A0--git=C2=A0a/devel/cbmc/pkg-descr=C2=A0b/devel/cbmc/pkg-descr
>=
=C2=A0
>=C2=A0new=C2=A0file=C2=A0mode=C2=A0100644
>=C2=A0
>=C2=A0inde=
x=C2=A0000000000000..2004194d7c43
>=C2=A0
>=C2=A0---=C2=A0/dev/null
>=
=C2=A0
>=C2=A0+++=C2=A0b/devel/cbmc/pkg-descr
>=C2=A0
>=C2=A0@@=C2=
=A0-0,0=C2=A0+1,7=C2=A0@@
>=C2=A0
>=C2=A0+CBMC=C2=A0is=C2=A0a=C2=A0Boun=
ded=C2=A0Model=C2=A0Checker=C2=A0for=C2=A0C=C2=A0and=C2=A0C++=C2=A0programs=
.
>=C2=A0
>=C2=A0+It=C2=A0supports=C2=A0C89,=C2=A0C99,=C2=A0most=C2=
=A0of=C2=A0C11=C2=A0and=C2=A0most=C2=A0compiler=C2=A0extensions=C2=A0provid=
ed=C2=A0by=C2=A0gcc
>=C2=A0
>=C2=A0+and=C2=A0Visual=C2=A0Studio.=C2=
=A0It=C2=A0allows=C2=A0verifying=C2=A0array=C2=A0bounds=C2=A0(buffer=C2=
=A0overflows),=C2=A0pointer
>=C2=A0
>=C2=A0+safety,=C2=A0exceptions=
=C2=A0and=C2=A0user-specified=C2=A0assertions.=C2=A0Furthermore,=C2=A0it=
=C2=A0can=C2=A0check=C2=A0C
>=C2=A0
>=C2=A0+and=C2=A0C++=C2=A0for=C2=
=A0consistency=C2=A0with=C2=A0other=C2=A0languages,=C2=A0such=C2=A0as=C2=
=A0Verilog.
>=C2=A0
>=C2=A0+The=C2=A0verification=C2=A0is=C2=A0performe=
d=C2=A0by=C2=A0unwinding=C2=A0the=C2=A0loops=C2=A0in=C2=A0the=C2=A0program=
=C2=A0and=C2=A0passing
>=C2=A0
>=C2=A0+the=C2=A0resulting=C2=A0equation=
=C2=A0to=C2=A0a=C2=A0decision=C2=A0procedure.
>=C2=A0
>=C2=A0diff=C2=
=A0--git=C2=A0a/devel/cbmc/pkg-plist=C2=A0b/devel/cbmc/pkg-plist
>=C2=
=A0
>=C2=A0new=C2=A0file=C2=A0mode=C2=A0100644
>=C2=A0
>=C2=A0index=
=C2=A0000000000000..2d23b585ef57
>=C2=A0
>=C2=A0---=C2=A0/dev/null
>=
=C2=A0
>=C2=A0+++=C2=A0b/devel/cbmc/pkg-plist
>=C2=A0
>=C2=A0@@=C2=
=A0-0,0=C2=A0+1,23=C2=A0@@
>=C2=A0
>=C2=A0+bin/cbmc
>=C2=A0
>=C2=
=A0+bin/crangler
>=C2=A0
>=C2=A0+bin/goto-analyzer
>=C2=A0
>=C2=
=A0+bin/goto-cc
>=C2=A0
>=C2=A0+bin/goto-diff
>=C2=A0
>=C2=A0+bin/g=
oto-instrument
>=C2=A0
>=C2=A0+bin/goto-inspect
>=C2=A0
>=C2=A0+bin=
/goto-harness
>=C2=A0
>=C2=A0+bin/goto-synthesizer
>=C2=A0
>=C2=
=A0+bin/symtab2gb
>=C2=A0
>=C2=A0+bin/ls_parse.py=C2=A0[http://parse.py=
]
>=C2=A0
>=C2=A0+bin/goto-gcc
>=C2=A0
>=C2=A0+bin/goto-ld
>=
=C2=A0
>=C2=A0+share/man/man1/cbmc.1.gz
>=C2=A0
>=C2=A0+share/man/man=
1/crangler.1.gz
>=C2=A0
>=C2=A0+share/man/man1/goto-analyzer.1.gz
>=
=C2=A0
>=C2=A0+share/man/man1/goto-cc.1.gz
>=C2=A0
>=C2=A0+share/man/=
man1/goto-diff.1.gz
>=C2=A0
>=C2=A0+share/man/man1/goto-harness.1.gz
=
>=C2=A0
>=C2=A0+share/man/man1/goto-inspect.1.gz
>=C2=A0
>=C2=A0+shar=
e/man/man1/goto-instrument.1.gz
>=C2=A0
>=C2=A0+share/man/man1/goto-syn=
thesizer.1.gz
>=C2=A0
>=C2=A0+share/man/man1/symtab2gb.1.gz

Hi,
=

Are these patches upstreamed or backported?

Best regards,

Dani=
el (diizzy@)



--_=_swift_1706832300_c2dcb94f2c2cc263794507f6574d26b4_=_
Content-Type: text/html; charset=utf-8
Content-Transfer-Encoding: quoted-printable

<div>On 2024-02-01T18:55:09.000+01:00, Olivier Cochard &lt;olivier@FreeBSD.=
org&gt; wrote:<br></div><div class=3D"ik_mail_quote answerContentMessage"><=
blockquote class=3D"ws-ng-quote"><pre style=3D"white-space: normal;"><div>T=
he branch main has been updated by olivier:<br></div><div><br></div><div>UR=
L: <a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMai=
lLink" href=3D"https://cgit.FreeBSD.org/ports/commit/?id=3D7f087b720e52d51b=
22db0da2d7565418a0e428ef" target=3D"_blank">https://cgit.FreeBSD.org/ports/=
commit/?id=3D7f087b720e52d51b22db0da2d7565418a0e428ef</a><br></div><div><br=
></div><div>commit 7f087b720e52d51b22db0da2d7565418a0e428ef<br></div><div>A=
uthor:     Olivier Cochard &lt;<a class=3D"defaultMailLink" href=3D"mailto:=
olivier@FreeBSD.org">olivier@FreeBSD.org</a>&gt;<br></div><div>AuthorDate: =
2024-02-01 17:50:02 +0000<br></div><div>Commit:     Olivier Cochard &lt;<a =
class=3D"defaultMailLink" href=3D"mailto:olivier@FreeBSD.org">olivier@FreeB=
SD.org</a>&gt;<br></div><div>CommitDate: 2024-02-01 17:53:55 +0000<br></div=
><div><br></div><div>    devel/cbmc: add new port<br></div><div>    <br></d=
iv><div>    Bounded Model Checker for C and C++ programs<br></div><div>    =
<a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMailLi=
nk" href=3D"https://github.com/diffblue/cbmc" target=3D"_blank">https://git=
hub.com/diffblue/cbmc</a><br></div><div>    <br></div><div>    Sponsored by=
:   Netflix<br></div><div>---<br></div><div> devel/Makefile                =
                     |  1 +<br></div><div> devel/cbmc/Makefile             =
                   | 46 +++++++++++++++++<br></div><div> devel/cbmc/distinf=
o                                |  5 ++<br></div><div> .../patch-minisat-2=
.2.1_minisat_core_<a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" clas=
s=3D"defaultMailLink" href=3D"http://Solver.cc" target=3D"_blank">Solver.cc=
</a>     | 20 ++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_core_=
SolverTypes.h | 59 ++++++++++++++++++++++<br></div><div> .../patch-minisat-=
2.2.1_minisat_mtl_IntTypes.h     | 12 +++++<br></div><div> .../files/patch-=
minisat-2.2.1_minisat_mtl_Vec.h    | 16 ++++++<br></div><div> .../files/pat=
ch-minisat-2.2.1_minisat_mtl_XAlloc.h | 19 +++++++<br></div><div> .../patch=
-minisat-2.2.1_minisat_simp_<a data-ik=3D"ik-secure" rel=3D"noopener norefe=
rrer" class=3D"defaultMailLink" href=3D"http://SimpSolver.cc" target=3D"_bl=
ank">SimpSolver.cc</a> | 37 ++++++++++++++<br></div><div> .../patch-minisat=
-2.2.1_minisat_utils_<a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" c=
lass=3D"defaultMailLink" href=3D"http://Options.cc" target=3D"_blank">Optio=
ns.cc</a>   | 15 ++++++<br></div><div> .../patch-minisat-2.2.1_minisat_util=
s_Options.h    | 30 +++++++++++<br></div><div> .../patch-minisat-2.2.1_mini=
sat_utils_ParseUtils.h | 33 ++++++++++++<br></div><div> .../patch-minisat-2=
.2.1_minisat_utils_System.h     | 11 ++++<br></div><div> devel/cbmc/files/p=
atch-src_common                  | 11 ++++<br></div><div> .../files/patch-s=
rc_solvers_sat_external__sat.cpp  | 13 +++++<br></div><div> devel/cbmc/file=
s/patch-src_util_optional.h         | 29 +++++++++++<br></div><div> devel/c=
bmc/pkg-descr                               |  7 +++<br></div><div> devel/c=
bmc/pkg-plist                               | 23 +++++++++<br></div><div> 1=
8 files changed, 387 insertions(+)<br></div><div><br></div><div>diff --git =
a/devel/Makefile b/devel/Makefile<br></div><div>index 4da71e0953a1..51481c8=
a3aca 100644<br></div><div>--- a/devel/Makefile<br></div><div>+++ b/devel/M=
akefile<br></div><div>@@ -351,6 +351,7 @@<br></div><div>     SUBDIR +=3D ca=
tch2<br></div><div>     SUBDIR +=3D cbang<br></div><div>     SUBDIR +=3D cb=
fmt<br></div><div>+    SUBDIR +=3D cbmc<br></div><div>     SUBDIR +=3D cbro=
wser<br></div><div>     SUBDIR +=3D cc65<br></div><div>     SUBDIR +=3D cca=
che<br></div><div>diff --git a/devel/cbmc/Makefile b/devel/cbmc/Makefile<br=
></div><div>new file mode 100644<br></div><div>index 000000000000..c7f7b365=
0e63<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/Makefile<br=
></div><div>@@ -0,0 +1,46 @@<br></div><div>+PORTNAME=3D=09cbmc<br></div><di=
v>+PORTVERSION=3D=095.95.1<br></div><div>+DISTVERSIONPREFIX=3D=09cbmc-<br><=
/div><div>+CATEGORIES=3D=09devel<br></div><div>+MASTER_SITES=3D=09DEBIAN/po=
ol/main/m/minisat2:minisat<br></div><div>+DISTFILES=3D=09minisat2_2.2.1.ori=
g.tar.gz:minisat<br></div><div>+<br></div><div>+MAINTAINER=3D=09<a class=3D=
"defaultMailLink" href=3D"mailto:olivier@FreeBSD.org">olivier@FreeBSD.org</=
a><br></div><div>+COMMENT=3D=09Bounded Model Checker for C and C++ programs=
<br></div><div>+WWW=3D=09=09<a data-ik=3D"ik-secure" rel=3D"noopener norefe=
rrer" class=3D"defaultMailLink" href=3D"https://github.com/diffblue/cbmc" t=
arget=3D"_blank">https://github.com/diffblue/cbmc</a><br></div><div>+<br></=
div><div>+LICENSE=3D=09BSD4CLAUSE<br></div><div>+LICENSE_FILE=3D=09${WRKSRC=
}/LICENSE<br></div><div>+<br></div><div>+BUILD_DEPENDS=3D=09${LOCALBASE}/bi=
n/flex:textproc/flex<br></div><div>+RUN_DEPENDS=3D=09${LOCALBASE}/bin/cvc5:=
math/cvc5 \<br></div><div>+=09=09${LOCALBASE}/bin/z3:math/z3<br></div><div>=
+<br></div><div>+USES=3D=09=09gmake bison python shebangfix<br></div><div>+=
<br></div><div>+USE_GITHUB=3D=09yes<br></div><div>+GH_ACCOUNT=3D=09diffblue=
<br></div><div>+SHEBANG_FILES=3D=09${WRKSRC}/scripts/ls_<a data-ik=3D"ik-se=
cure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" href=3D"http://=
parse.py" target=3D"_blank">parse.py</a><br></div><div>+WRKSRC_minisat=3D=
=09${WRKDIR}/minisat2-2.2.1<br></div><div>+<br></div><div>+post-patch:<br><=
/div><div>+=09@${REINPLACE_CMD} -e 's|.*git describe --tags.*|GIT_INFO =3D =
${PORTNAME}-${PORTVERSION}|' \<br></div><div>+=09=09${WRKSRC}/src/util/Make=
file<br></div><div>+post-extract:<br></div><div>+=09@${MV} ${WRKSRC_minisat=
} ${WRKSRC}/minisat-2.2.1<br></div><div>+<br></div><div>+do-build:<br></div=
><div>+=09@${MKDIR} ${STAGEDIR}<br></div><div>+=09cd ${WRKSRC} &amp;&amp; $=
{GMAKE} -C src -j${MAKE_JOBS_NUMBER}<br></div><div>+<br></div><div>+do-inst=
all:<br></div><div>+.  for x in cbmc crangler goto-analyzer goto-cc goto-di=
ff goto-instrument \<br></div><div>+=09goto-inspect goto-harness goto-synth=
esizer symtab2gb<br></div><div>+=09${INSTALL_PROGRAM} ${WRKSRC}/src/${x}/${=
x} ${STAGEDIR}${PREFIX}/bin/<br></div><div>+=09${INSTALL_MAN} ${WRKSRC}/doc=
/man/${x}.1 ${STAGEDIR}${PREFIX}/share/man/man1/<br></div><div>+.  endfor<b=
r></div><div>+=09${LN} -sf goto-cc ${STAGEDIR}${PREFIX}/bin/goto-gcc<br></d=
iv><div>+=09${LN} -sf goto-cc ${STAGEDIR}${PREFIX}/bin/goto-ld<br></div><di=
v>+=09${INSTALL_SCRIPT} ${WRKSRC}/scripts/ls_<a data-ik=3D"ik-secure" rel=
=3D"noopener noreferrer" class=3D"defaultMailLink" href=3D"http://parse.py"=
 target=3D"_blank">parse.py</a> ${STAGEDIR}${PREFIX}/bin/<br></div><div>+<b=
r></div><div>+.include &lt;<a data-ik=3D"ik-secure" rel=3D"noopener norefer=
rer" class=3D"defaultMailLink" href=3D"http://bsd.port.mk>" target=3D"_blan=
k">bsd.port.mk&gt;</a>;<br></div><div>diff --git a/devel/cbmc/distinfo b/de=
vel/cbmc/distinfo<br></div><div>new file mode 100644<br></div><div>index 00=
0000000000..f3e6d1161c6a<br></div><div>--- /dev/null<br></div><div>+++ b/de=
vel/cbmc/distinfo<br></div><div>@@ -0,0 +1,5 @@<br></div><div>+TIMESTAMP =
=3D 1706723199<br></div><div>+SHA256 (minisat2_2.2.1.orig.tar.gz) =3D e54af=
a3c192c1753bc8075c0c7e126d5c495d9066e3f90a2588091149ac9ca40<br></div><div>+=
SIZE (minisat2_2.2.1.orig.tar.gz) =3D 44229<br></div><div>+SHA256 (diffblue=
-cbmc-cbmc-5.95.1_GH0.tar.gz) =3D fdc1e862752430f8d069eb2f9c33dcd05078cf955=
bbc900e2cc840bcb01b3783<br></div><div>+SIZE (diffblue-cbmc-cbmc-5.95.1_GH0.=
tar.gz) =3D 9073428<br></div><div>diff --git a/devel/cbmc/files/patch-minis=
at-2.2.1_minisat_core_<a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" =
class=3D"defaultMailLink" href=3D"http://Solver.cc" target=3D"_blank">Solve=
r.cc</a> b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_<a data-ik=3D"=
ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" href=3D"ht=
tp://Solver.cc" target=3D"_blank">Solver.cc</a><br></div><div>new file mode=
 100644<br></div><div>index 000000000000..c15c2f12fb0a<br></div><div>--- /d=
ev/null<br></div><div>+++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_co=
re_<a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMai=
lLink" href=3D"http://Solver.cc" target=3D"_blank">Solver.cc</a><br></div><=
div>@@ -0,0 +1,20 @@<br></div><div>+--- minisat-2.2.1/minisat/core/<a data-=
ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" href=
=3D"http://Solver.cc.orig" target=3D"_blank">Solver.cc.orig</a>=092011-02-2=
1 13:31:17 UTC<br></div><div>++++ minisat-2.2.1/minisat/core/<a data-ik=3D"=
ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" href=3D"ht=
tp://Solver.cc" target=3D"_blank">Solver.cc</a><br></div><div>+@@ -210,7 +2=
10,7 @@ void Solver::cancelUntil(int level) {<br></div><div>+         for (=
int c =3D trail.size()-1; c &amp;gt;=3D trail_lim[level]; c--){<br></div><d=
iv>+             Var      x  =3D var(trail[c]);<br></div><div>+            =
 assigns [x] =3D l_Undef;<br></div><div>+-            if (phase_saving &gt;=
 1 || (phase_saving =3D=3D 1) &amp;&amp; c &gt; trail_lim.last())<br></div>=
<div>++            if (phase_saving &gt; 1 || ((phase_saving =3D=3D 1) &amp=
;&amp; c &gt; trail_lim.last()))<br></div><div>+                 polarity[x=
] =3D sign(trail[c]);<br></div><div>+             insertVarOrder(x); }<br><=
/div><div>+         qhead =3D trail_lim[level];<br></div><div>+@@ -666,7 +6=
66,7 @@ lbool Solver::search(int nof_conflicts)<br></div><div>+ <br></div><=
div>+         }else{<br></div><div>+             // NO CONFLICT<br></div><d=
iv>+-            if (nof_conflicts &amp;gt;=3D 0 &amp;&amp; conflictC &amp;=
gt;=3D nof_conflicts || !withinBudget()){<br></div><div>++            if ((=
nof_conflicts &amp;gt;=3D 0 &amp;&amp; conflictC &amp;gt;=3D nof_conflicts)=
 || !withinBudget()){<br></div><div>+                 // Reached bound on n=
umber of conflicts:<br></div><div>+                 progress_estimate =3D p=
rogressEstimate();<br></div><div>+                 cancelUntil(0);<br></div=
><div>diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver=
Types.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h<b=
r></div><div>new file mode 100644<br></div><div>index 000000000000..fa26c63=
72b36<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/files/patc=
h-minisat-2.2.1_minisat_core_SolverTypes.h<br></div><div>@@ -0,0 +1,59 @@<b=
r></div><div>+--- minisat-2.2.1/minisat/core/SolverTypes.h.orig=092011-02-2=
1 13:31:17 UTC<br></div><div>++++ minisat-2.2.1/minisat/core/SolverTypes.h<=
br></div><div>+@@ -47,7 +47,7 @@ struct Lit {<br></div><div>+     int     x=
;<br></div><div>+ <br></div><div>+     // Use this as a constructor:<br></d=
iv><div>+-    friend Lit mkLit(Var var, bool sign =3D false);<br></div><div=
>++    //friend Lit mkLit(Var var, bool sign =3D false);<br></div><div>+ <b=
r></div><div>+     bool operator =3D=3D (Lit p) const { return x =3D=3D p.x=
; }<br></div><div>+     bool operator !=3D (Lit p) const { return x !=3D p.=
x; }<br></div><div>+@@ -55,7 +55,7 @@ struct Lit {<br></div><div>+ };<br></=
div><div>+ <br></div><div>+ <br></div><div>+-inline  Lit  mkLit     (Var va=
r, bool sign) { Lit p; p.x =3D var + var + (int)sign; return p; }<br></div>=
<div>++inline  Lit  mkLit     (Var var, bool sign =3D false) { Lit p; p.x =
=3D var + var + (int)sign; return p; }<br></div><div>+ inline  Lit  operato=
r ~(Lit p)              { Lit q; q.x =3D p.x ^ 1; return q; }<br></div><div=
>+ inline  Lit  operator ^(Lit p, bool b)      { Lit q; q.x =3D p.x ^ (unsi=
gned int)b; return q; }<br></div><div>+ inline  bool sign      (Lit p)     =
         { return p.x &amp; 1; }<br></div><div>+@@ -127,7 +127,10 @@ class =
Clause {<br></div><div>+         unsigned has_extra : 1;<br></div><div>+   =
      unsigned reloced   : 1;<br></div><div>+         unsigned size      : =
27; }                        header;<br></div><div>++#include &lt;util/prag=
ma_push.def&gt;<br></div><div>++#include &lt;util/pragma_wzero_length_array=
.def&gt;<br></div><div>+     union { Lit lit; float act; uint32_t abs; CRef=
 rel; } data[0];<br></div><div>++#include &lt;util/pragma_pop.def&gt;<br></=
div><div>+ <br></div><div>+     friend class ClauseAllocator;<br></div><div=
>+ <br></div><div>+@@ -142,11 +145,12 @@ class Clause {<br></div><div>+    =
     for (int i =3D 0; i &lt; ps.size(); i++) <br></div><div>+             =
data[i].lit =3D ps[i];<br></div><div>+ <br></div><div>+-        if (header.=
has_extra)<br></div><div>++        if (header.has_extra) {<br></div><div>+ =
            if (header.learnt)<br></div><div>+                 data[header.=
size].act =3D 0;<br></div><div>+             else<br></div><div>+          =
       calcAbstraction();<br></div><div>++        }<br></div><div>+     }<b=
r></div><div>+ <br></div><div>+     // NOTE: This constructor cannot be use=
d directly (doesn't allocate enough memory).<br></div><div>+@@ -157,11 +161=
,12 @@ class Clause {<br></div><div>+         for (int i =3D 0; i &lt; from=
.size(); i++)<br></div><div>+             data[i].lit =3D from[i];<br></div=
><div>+ <br></div><div>+-        if (header.has_extra)<br></div><div>++    =
    if (header.has_extra) {<br></div><div>+             if (header.learnt)<=
br></div><div>+                 data[header.size].act =3D <a data-ik=3D"ik-=
secure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" href=3D"http:=
//from.data[header.size]" target=3D"_blank">from.data[header.size]</a>.act;=
<br></div><div>+             else <br></div><div>+                 data[hea=
der.size].abs =3D <a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" clas=
s=3D"defaultMailLink" href=3D"http://from.data[header.size]" target=3D"_bla=
nk">from.data[header.size]</a>.abs;<br></div><div>++        }<br></div><div=
>+     }<br></div><div>+ <br></div><div>+ public:<br></div><div>diff --git =
a/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h b/devel/cbmc/=
files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h<br></div><div>new file mod=
e 100644<br></div><div>index 000000000000..d8c9ddedb701<br></div><div>--- /=
dev/null<br></div><div>+++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_m=
tl_IntTypes.h<br></div><div>@@ -0,0 +1,12 @@<br></div><div>+--- minisat-2.2=
.1/minisat/mtl/IntTypes.h.orig=092011-02-21 13:31:17 UTC<br></div><div>++++=
 minisat-2.2.1/minisat/mtl/IntTypes.h<br></div><div>+@@ -31,7 +31,9 @@ OF O=
R IN CONNECTION WITH THE SOFTWARE OR THE USE OR OT<br></div><div>+ #else<br=
></div><div>+ <br></div><div>+ #   include &lt;stdint.h&gt;<br></div><div>+=
+#ifndef _MSC_VER<br></div><div>+ #   include &lt;inttypes.h&gt;<br></div><=
div>++#endif<br></div><div>+ <br></div><div>+ The branch main has been upda=
ted by olivier:<br></div><div><br></div><div>URL: <a data-ik=3D"ik-secure" =
rel=3D"noopener noreferrer" class=3D"defaultMailLink" href=3D"https://cgit.=
FreeBSD.org/ports/commit/?id=3D7f087b720e52d51b22db0da2d7565418a0e428ef" ta=
rget=3D"_blank">https://cgit.FreeBSD.org/ports/commit/?id=3D7f087b720e52d51=
b22db0da2d7565418a0e428ef</a><br></div><div><br></div><div>commit 7f087b720=
e52d51b22db0da2d7565418a0e428ef<br></div><div>Author:     Olivier Cochard &=
lt;<a class=3D"defaultMailLink" href=3D"mailto:olivier@FreeBSD.org">olivier=
@FreeBSD.org</a>&gt;<br></div><div>AuthorDate: 2024-02-01 17:50:02 +0000<br=
></div><div>Commit:     Olivier Cochard &lt;<a class=3D"defaultMailLink" hr=
ef=3D"mailto:olivier@FreeBSD.org">olivier@FreeBSD.org</a>&gt;<br></div><div=
>CommitDate: 2024-02-01 17:53:55 +0000<br></div><div><br></div><div>    dev=
el/cbmc: add new port<br></div><div>    <br></div><div>    Bounded Model Ch=
ecker for C and C++ programs<br></div><div>    <a data-ik=3D"ik-secure" rel=
=3D"noopener noreferrer" class=3D"defaultMailLink" href=3D"https://github.c=
om/diffblue/cbmc" target=3D"_blank">https://github.com/diffblue/cbmc</a><br=
></div><div>    <br></div><div>    Sponsored by:   Netflix<br></div><div>--=
-<br></div><div> devel/Makefile                                     |  1 +<=
br></div><div> devel/cbmc/Makefile                                | 46 ++++=
+++++++++++++<br></div><div> devel/cbmc/distinfo                           =
     |  5 ++<br></div><div> .../patch-minisat-2.2.1_minisat_core_<a data-ik=
=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" href=
=3D"http://Solver.cc" target=3D"_blank">Solver.cc</a>     | 20 ++++++++<br>=
</div><div> .../patch-minisat-2.2.1_minisat_core_SolverTypes.h | 59 +++++++=
+++++++++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_mtl_IntTypes=
.h     | 12 +++++<br></div><div> .../files/patch-minisat-2.2.1_minisat_mtl_=
Vec.h    | 16 ++++++<br></div><div> .../files/patch-minisat-2.2.1_minisat_m=
tl_XAlloc.h | 19 +++++++<br></div><div> .../patch-minisat-2.2.1_minisat_sim=
p_<a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMail=
Link" href=3D"http://SimpSolver.cc" target=3D"_blank">SimpSolver.cc</a> | 3=
7 ++++++++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_utils_<a da=
ta-ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" h=
ref=3D"http://Options.cc" target=3D"_blank">Options.cc</a>   | 15 ++++++<br=
></div><div> .../patch-minisat-2.2.1_minisat_utils_Options.h    | 30 ++++++=
+++++<br></div><div> .../patch-minisat-2.2.1_minisat_utils_ParseUtils.h | 3=
3 ++++++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_utils_System.=
h     | 11 ++++<br></div><div> devel/cbmc/files/patch-src_common           =
       | 11 ++++<br></div><div> .../files/patch-src_solvers_sat_external__s=
at.cpp  | 13 +++++<br></div><div> devel/cbmc/files/patch-src_util_optional.=
h         | 29 +++++++++++<br></div><div> devel/cbmc/pkg-descr             =
                  |  7 +++<br></div><div> devel/cbmc/pkg-plist             =
                  | 23 +++++++++<br></div><div> 18 files changed, 387 inser=
tions(+)<br></div><div><br></div><div>diff --git a/devel/Makefile b/devel/M=
akefile<br></div><div>index 4da71e0953a1..51481c8a3aca 100644<br></div><div=
>--- a/devel/Makefile<br></div><div>+++ b/devel/Makefile<br></div><div>@@ -=
351,6 +351,7 @@<br></div><div>     SUBDIR +=3D catch2<br></div><div>     SU=
BDIR +=3D cbang<br></div><div>     SUBDIR +=3D cbfmt<br></div><div>+    SUB=
DIR +=3D cbmc<br></div><div>     SUBDIR +=3D cbrowser<br></div><div>     SU=
BDIR +=3D cc65<br></div><div>     SUBDIR +=3D ccache<br></div><div>diff --g=
it a/devel/cbmc/Makefile b/devel/cbmc/Makefile<br></div><div>new file mode =
100644<br></div><div>index 000000000000..c7f7b3650e63<br></div><div>--- /de=
v/null<br></div><div>+++ b/devel/cbmc/Makefile<br></div><div>@@ -0,0 +1,46 =
@@<br></div><div>+PORTNAME=3D=09cbmc<br></div><div>+PORTVERSION=3D=095.95.1=
<br></div><div>+DISTVERSIONPREFIX=3D=09cbmc-<br></div><div>+CATEGORIES=3D=
=09devel<br></div><div>+MASTER_SITES=3D=09DEBIAN/pool/main/m/minisat2:minis=
at<br></div><div>+DISTFILES=3D=09minisat2_2.2.1.orig.tar.gz:minisat<br></di=
v><div>+<br></div><div>+MAINTAINER=3D=09<a class=3D"defaultMailLink" href=
=3D"mailto:olivier@FreeBSD.org">olivier@FreeBSD.org</a><br></div><div>+COMM=
ENT=3D=09Bounded Model Checker for C and C++ programs<br></div><div>+WWW=3D=
=09=09<a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"default=
MailLink" href=3D"https://github.com/diffblue/cbmc" target=3D"_blank">https=
://github.com/diffblue/cbmc</a><br></div><div>+<br></div><div>+LICENSE=3D=
=09BSD4CLAUSE<br></div><div>+LICENSE_FILE=3D=09${WRKSRC}/LICENSE<br></div><=
div>+<br></div><div>+BUILD_DEPENDS=3D=09${LOCALBASE}/bin/flex:textproc/flex=
<br></div><div>+RUN_DEPENDS=3D=09${LOCALBASE}/bin/cvc5:math/cvc5 \<br></div=
><div>+=09=09${LOCALBASE}/bin/z3:math/z3<br></div><div>+<br></div><div>+USE=
S=3D=09=09gmake bison python shebangfix<br></div><div>+<br></div><div>+USE_=
GITHUB=3D=09yes<br></div><div>+GH_ACCOUNT=3D=09diffblue<br></div><div>+SHEB=
ANG_FILES=3D=09${WRKSRC}/scripts/ls_<a data-ik=3D"ik-secure" rel=3D"noopene=
r noreferrer" class=3D"defaultMailLink" href=3D"http://parse.py" target=3D"=
_blank">parse.py</a><br></div><div>+WRKSRC_minisat=3D=09${WRKDIR}/minisat2-=
2.2.1<br></div><div>+<br></div><div>+post-patch:<br></div><div>+=09@${REINP=
LACE_CMD} -e 's|.*git describe --tags.*|GIT_INFO =3D ${PORTNAME}-${PORTVERS=
ION}|' \<br></div><div>+=09=09${WRKSRC}/src/util/Makefile<br></div><div>+po=
st-extract:<br></div><div>+=09@${MV} ${WRKSRC_minisat} ${WRKSRC}/minisat-2.=
2.1<br></div><div>+<br></div><div>+do-build:<br></div><div>+=09@${MKDIR} ${=
STAGEDIR}<br></div><div>+=09cd ${WRKSRC} &amp;&amp; ${GMAKE} -C src -j${MAK=
E_JOBS_NUMBER}<br></div><div>+<br></div><div>+do-install:<br></div><div>+. =
 for x in cbmc crangler goto-analyzer goto-cc goto-diff goto-instrument \<b=
r></div><div>+=09goto-inspect goto-harness goto-synthesizer symtab2gb<br></=
div><div>+=09${INSTALL_PROGRAM} ${WRKSRC}/src/${x}/${x} ${STAGEDIR}${PREFIX=
}/bin/<br></div><div>+=09${INSTALL_MAN} ${WRKSRC}/doc/man/${x}.1 ${STAGEDIR=
}${PREFIX}/share/man/man1/<br></div><div>+.  endfor<br></div><div>+=09${LN}=
 -sf goto-cc ${STAGEDIR}${PREFIX}/bin/goto-gcc<br></div><div>+=09${LN} -sf =
goto-cc ${STAGEDIR}${PREFIX}/bin/goto-ld<br></div><div>+=09${INSTALL_SCRIPT=
} ${WRKSRC}/scripts/ls_<a data-ik=3D"ik-secure" rel=3D"noopener noreferrer"=
 class=3D"defaultMailLink" href=3D"http://parse.py" target=3D"_blank">parse=
.py</a> ${STAGEDIR}${PREFIX}/bin/<br></div><div>+<br></div><div>+.include &=
lt;<a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMai=
lLink" href=3D"http://bsd.port.mk>" target=3D"_blank">bsd.port.mk&gt;</a>;<=
br></div><div>diff --git a/devel/cbmc/distinfo b/devel/cbmc/distinfo<br></d=
iv><div>new file mode 100644<br></div><div>index 000000000000..f3e6d1161c6a=
<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/distinfo<br></d=
iv><div>@@ -0,0 +1,5 @@<br></div><div>+TIMESTAMP =3D 1706723199<br></div><d=
iv>+SHA256 (minisat2_2.2.1.orig.tar.gz) =3D e54afa3c192c1753bc8075c0c7e126d=
5c495d9066e3f90a2588091149ac9ca40<br></div><div>+SIZE (minisat2_2.2.1.orig.=
tar.gz) =3D 44229<br></div><div>+SHA256 (diffblue-cbmc-cbmc-5.95.1_GH0.tar.=
gz) =3D fdc1e862752430f8d069eb2f9c33dcd05078cf955bbc900e2cc840bcb01b3783<br=
></div><div>+SIZE (diffblue-cbmc-cbmc-5.95.1_GH0.tar.gz) =3D 9073428<br></d=
iv><div>diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_<a d=
ata-ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" =
href=3D"http://Solver.cc" target=3D"_blank">Solver.cc</a> b/devel/cbmc/file=
s/patch-minisat-2.2.1_minisat_core_<a data-ik=3D"ik-secure" rel=3D"noopener=
 noreferrer" class=3D"defaultMailLink" href=3D"http://Solver.cc" target=3D"=
_blank">Solver.cc</a><br></div><div>new file mode 100644<br></div><div>inde=
x 000000000000..c15c2f12fb0a<br></div><div>--- /dev/null<br></div><div>+++ =
b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_<a data-ik=3D"ik-secure=
" rel=3D"noopener noreferrer" class=3D"defaultMailLink" href=3D"http://Solv=
er.cc" target=3D"_blank">Solver.cc</a><br></div><div>@@ -0,0 +1,20 @@<br></=
div><div>+--- minisat-2.2.1/minisat/core/<a data-ik=3D"ik-secure" rel=3D"no=
opener noreferrer" class=3D"defaultMailLink" href=3D"http://Solver.cc.orig"=
 target=3D"_blank">Solver.cc.orig</a>=092011-02-21 13:31:17 UTC<br></div><d=
iv>++++ minisat-2.2.1/minisat/core/<a data-ik=3D"ik-secure" rel=3D"noopener=
 noreferrer" class=3D"defaultMailLink" href=3D"http://Solver.cc" target=3D"=
_blank">Solver.cc</a><br></div><div>+@@ -210,7 +210,7 @@ void Solver::cance=
lUntil(int level) {<br></div><div>+         for (int c =3D trail.size()-1; =
c &amp;gt;=3D trail_lim[level]; c--){<br></div><div>+             Var      =
x  =3D var(trail[c]);<br></div><div>+             assigns [x] =3D l_Undef;<=
br></div><div>+-            if (phase_saving &gt; 1 || (phase_saving =3D=3D=
 1) &amp;&amp; c &gt; trail_lim.last())<br></div><div>++            if (pha=
se_saving &gt; 1 || ((phase_saving =3D=3D 1) &amp;&amp; c &gt; trail_lim.la=
st()))<br></div><div>+                 polarity[x] =3D sign(trail[c]);<br><=
/div><div>+             insertVarOrder(x); }<br></div><div>+         qhead =
=3D trail_lim[level];<br></div><div>+@@ -666,7 +666,7 @@ lbool Solver::sear=
ch(int nof_conflicts)<br></div><div>+ <br></div><div>+         }else{<br></=
div><div>+             // NO CONFLICT<br></div><div>+-            if (nof_c=
onflicts &amp;gt;=3D 0 &amp;&amp; conflictC &amp;gt;=3D nof_conflicts || !w=
ithinBudget()){<br></div><div>++            if ((nof_conflicts &amp;gt;=3D =
0 &amp;&amp; conflictC &amp;gt;=3D nof_conflicts) || !withinBudget()){<br><=
/div><div>+                 // Reached bound on number of conflicts:<br></d=
iv><div>+                 progress_estimate =3D progressEstimate();<br></di=
v><div>+                 cancelUntil(0);<br></div><div>diff --git a/devel/c=
bmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h b/devel/cbmc/files=
/patch-minisat-2.2.1_minisat_core_SolverTypes.h<br></div><div>new file mode=
 100644<br></div><div>index 000000000000..fa26c6372b36<br></div><div>--- /d=
ev/null<br></div><div>+++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_co=
re_SolverTypes.h<br></div><div>@@ -0,0 +1,59 @@<br></div><div>+--- minisat-=
2.2.1/minisat/core/SolverTypes.h.orig=092011-02-21 13:31:17 UTC<br></div><d=
iv>++++ minisat-2.2.1/minisat/core/SolverTypes.h<br></div><div>+@@ -47,7 +4=
7,7 @@ struct Lit {<br></div><div>+     int     x;<br></div><div>+ <br></di=
v><div>+     // Use this as a constructor:<br></div><div>+-    friend Lit m=
kLit(Var var, bool sign =3D false);<br></div><div>++    //friend Lit mkLit(=
Var var, bool sign =3D false);<br></div><div>+ <br></div><div>+     bool op=
erator =3D=3D (Lit p) const { return x =3D=3D p.x; }<br></div><div>+     bo=
ol operator !=3D (Lit p) const { return x !=3D p.x; }<br></div><div>+@@ -55=
,7 +55,7 @@ struct Lit {<br></div><div>+ };<br></div><div>+ <br></div><div>=
+ <br></div><div>+-inline  Lit  mkLit     (Var var, bool sign) { Lit p; p.x=
 =3D var + var + (int)sign; return p; }<br></div><div>++inline  Lit  mkLit =
    (Var var, bool sign =3D false) { Lit p; p.x =3D var + var + (int)sign; =
return p; }<br></div><div>+ inline  Lit  operator ~(Lit p)              { L=
it q; q.x =3D p.x ^ 1; return q; }<br></div><div>+ inline  Lit  operator ^(=
Lit p, bool b)      { Lit q; q.x =3D p.x ^ (unsigned int)b; return q; }<br>=
</div><div>+ inline  bool sign      (Lit p)              { return p.x &amp;=
 1; }<br></div><div>+@@ -127,7 +127,10 @@ class Clause {<br></div><div>+   =
      unsigned has_extra : 1;<br></div><div>+         unsigned reloced   : =
1;<br></div><div>+         unsigned size      : 27; }                      =
  header;<br></div><div>++#include &lt;util/pragma_push.def&gt;<br></div><d=
iv>++#include &lt;util/pragma_wzero_length_array.def&gt;<br></div><div>+   =
  union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];<br></div><=
div>++#include &lt;util/pragma_pop.def&gt;<br></div><div>+ <br></div><div>+=
     friend class ClauseAllocator;<br></div><div>+ <br></div><div>+@@ -142,=
11 +145,12 @@ class Clause {<br></div><div>+         for (int i =3D 0; i &l=
t; ps.size(); i++) <br></div><div>+             data[i].lit =3D ps[i];<br><=
/div><div>+ <br></div><div>+-        if (header.has_extra)<br></div><div>++=
        if (header.has_extra) {<br></div><div>+             if (header.lear=
nt)<br></div><div>+                 data[header.size].act =3D 0;<br></div><=
div>+             else<br></div><div>+                 calcAbstraction();<b=
r></div><div>++        }<br></div><div>+     }<br></div><div>+ <br></div><d=
iv>+     // NOTE: This constructor cannot be used directly (doesn't allocat=
e enough memory).<br></div><div>+@@ -157,11 +161,12 @@ class Clause {<br></=
div><div>+         for (int i =3D 0; i &lt; from.size(); i++)<br></div><div=
>+             data[i].lit =3D from[i];<br></div><div>+ <br></div><div>+-  =
      if (header.has_extra)<br></div><div>++        if (header.has_extra) {=
<br></div><div>+             if (header.learnt)<br></div><div>+            =
     data[header.size].act =3D <a data-ik=3D"ik-secure" rel=3D"noopener nor=
eferrer" class=3D"defaultMailLink" href=3D"http://from.data[header.size]" t=
arget=3D"_blank">from.data[header.size]</a>.act;<br></div><div>+           =
  else <br></div><div>+                 data[header.size].abs =3D <a data-i=
k=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" href=
=3D"http://from.data[header.size]" target=3D"_blank">from.data[header.size]=
</a>.abs;<br></div><div>++        }<br></div><div>+     }<br></div><div>+ <=
br></div><div>+ public:<br></div><div>diff --git a/devel/cbmc/files/patch-m=
inisat-2.2.1_minisat_mtl_IntTypes.h b/devel/cbmc/files/patch-minisat-2.2.1_=
minisat_mtl_IntTypes.h<br></div><div>new file mode 100644<br></div><div>ind=
ex 000000000000..d8c9ddedb701<br></div><div>--- /dev/null<br></div><div>+++=
 b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h<br></div><di=
v>@@ -0,0 +1,12 @@<br></div><div>+--- minisat-2.2.1/minisat/mtl/IntTypes.h.=
orig=092011-02-21 13:31:17 UTC<br></div><div>++++ minisat-2.2.1/minisat/mtl=
/IntTypes.h<br></div><div>+@@ -31,7 +31,9 @@ OF OR IN CONNECTION WITH THE S=
OFTWARE OR THE USE OR OT<br></div><div>+ #else<br></div><div>+ <br></div><d=
iv>+ #   include &lt;stdint.h&gt;<br></div><div>++#ifndef _MSC_VER<br></div=
><div>+ #   include &lt;inttypes.h&gt;<br></div><div>++#endif<br></div><div=
>+ <br></div><div>+ #endiffile mode 100644<br></div><div>index 000000000000=
..f0dd61cd9963<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/f=
iles/patch-src_solvers_sat_external__sat.cpp<br></div><div>@@ -0,0 +1,13 @@=
<br></div><div>+--- src/solvers/sat/external_sat.cpp.orig=092023-10-30 12:1=
1:18 UTC<br></div><div>++++ src/solvers/sat/external_sat.cpp<br></div><div>=
+@@ -119,8 +119,8 @@ external_satt::resultt external_satt::parse_result(std=
<br></div><div>+       {<br></div><div>+         try<br></div><div>+       =
  {<br></div><div>+-          signed long long as_long =3D std::stol(assign=
ment_string);<br></div><div>+-          size_t index =3D std::labs(as_long)=
;<br></div><div>++          signed long long as_long =3D std::stoll(assignm=
ent_string);<br></div><div>++          size_t index =3D std::llabs(as_long)=
;<br></div><div>+ <br></div><div>+           if(index &amp;gt;=3D number_of=
_variables)<br></div><div>+           {<br></div><div>diff --git a/devel/cb=
mc/files/patch-src_util_optional.h b/devel/cbmc/files/patch-src_util_option=
al.h<br></div><div>new file mode 100644<br></div><div>index 000000000000..4=
507ce0ade2b<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/file=
s/patch-src_util_optional.h<br></div><div>@@ -0,0 +1,29 @@<br></div><div>+-=
-- src/util/optional.h.orig=092023-10-30 12:11:18 UTC<br></div><div>++++ sr=
c/util/optional.h<br></div><div>+@@ -11,20 +11,20 @@ Author: Diffblue Ltd.<=
br></div><div>+ #define CPROVER_UTIL_OPTIONAL_H<br></div><div>+ <br></div><=
div>+ #if defined __clang__<br></div><div>+-  #pragma clang diagnostic push=
 ignore "-Wall"<br></div><div>+-  #pragma clang diagnostic push ignore "-Wp=
edantic"<br></div><div>++  #pragma clang diagnostic push<br></div><div>++  =
#pragma clang diagnostic ignored "-Wall"<br></div><div>++  #pragma clang di=
agnostic ignored "-Wpedantic"<br></div><div>+ #elif defined __GNUC__<br></d=
iv><div>+-  #pragma GCC diagnostic push ignore "-Wall"<br></div><div>+-  #p=
ragma GCC diagnostic push ignore "-Wpedantic"<br></div><div>++  #pragma GCC=
 diagnostic push<br></div><div>++  #pragma GCC diagnostic ignored "-Wall"<b=
r></div><div>++  #pragma GCC diagnostic ignored "-Wpedantic"<br></div><div>=
+ #elif defined _MSC_VER<br></div><div>+   #pragma warning(push)<br></div><=
div>+ #endif<br></div><div>+ #include &lt;nonstd/optional.hpp&gt;<br></div>=
<div>+ #if defined  __clang__<br></div><div>+   #pragma clang diagnostic po=
p<br></div><div>+-  #pragma clang diagnostic pop<br></div><div>+ #elif defi=
ned  __GNUC__<br></div><div>+-  #pragma GCC diagnostic pop<br></div><div>+ =
  #pragma GCC diagnostic pop<br></div><div>+ #elif defined _MSC_VER<br></di=
v><div>+   #pragma warning(pop)<br></div><div>diff --git a/devel/cbmc/pkg-d=
escr b/devel/cbmc/pkg-descr<br></div><div>new file mode 100644<br></div><di=
v>index 000000000000..2004194d7c43<br></div><div>--- /dev/null<br></div><di=
v>+++ b/devel/cbmc/pkg-descr<br></div><div>@@ -0,0 +1,7 @@<br></div><div>+C=
BMC is a Bounded Model Checker for C and C++ programs.<br></div><div>+It su=
pports C89, C99, most of C11 and most compiler extensions provided by gcc<b=
r></div><div>+and Visual Studio. It allows verifying array bounds (buffer o=
verflows), pointer<br></div><div>+safety, exceptions and user-specified ass=
ertions. Furthermore, it can check C<br></div><div>+and C++ for consistency=
 with other languages, such as Verilog.<br></div><div>+The verification is =
performed by unwinding the loops in the program and passing<br></div><div>+=
the resulting equation to a decision procedure.<br></div><div>diff --git a/=
devel/cbmc/pkg-plist b/devel/cbmc/pkg-plist<br></div><div>new file mode 100=
644<br></div><div>index 000000000000..2d23b585ef57<br></div><div>--- /dev/n=
ull<br></div><div>+++ b/devel/cbmc/pkg-plist<br></div><div>@@ -0,0 +1,23 @@=
<br></div><div>+bin/cbmc<br></div><div>+bin/crangler<br></div><div>+bin/got=
o-analyzer<br></div><div>+bin/goto-cc<br></div><div>+bin/goto-diff<br></div=
><div>+bin/goto-instrument<br></div><div>+bin/goto-inspect<br></div><div>+b=
in/goto-harness<br></div><div>+bin/goto-synthesizer<br></div><div>+bin/symt=
ab2gb<br></div><div>+bin/ls_<a data-ik=3D"ik-secure" rel=3D"noopener norefe=
rrer" class=3D"defaultMailLink" href=3D"http://parse.py" target=3D"_blank">=
parse.py</a><br></div><div>+bin/goto-gcc<br></div><div>+bin/goto-ld<br></di=
v><div>+share/man/man1/cbmc.1.gz<br></div><div>+share/man/man1/crangler.1.g=
z<br></div><div>+share/man/man1/goto-analyzer.1.gz<br></div><div>+share/man=
/man1/goto-cc.1.gz<br></div><div>+share/man/man1/goto-diff.1.gz<br></div><d=
iv>+share/man/man1/goto-harness.1.gz<br></div><div>+share/man/man1/goto-ins=
pect.1.gz<br></div><div>+share/man/man1/goto-instrument.1.gz<br></div><div>=
+share/man/man1/goto-synthesizer.1.gz<br></div><div>+share/man/man1/symtab2=
gb.1.gz<br></div></pre></blockquote></div><div>Hi,<br></div><div><br></div>=
<div>Are these patches upstreamed or backported?<br></div><div><br></div><d=
iv>Best regards,<br></div><div>Daniel (diizzy@)<br></div><div ><div><br></d=
iv></div>


--_=_swift_1706832300_c2dcb94f2c2cc263794507f6574d26b4_=_--