STP imports code from the following libraries:
	* Bit::Vector Copyright (c) 1995 - 2004 by Steffen Beyer. 
	* CVC's SMT-LIB Parser  Copyright (C) 2004 by the Board of Trustees
		of Leland Stanford Junior University and by New York University.
	* ABC Copyright (c) The Regents of the University of California.
	* mimalloc Copyright (c) 2018-2025 Microsoft Corporation, Daan Leijen.
	* ankerl::unordered_dense Copyright (c) 2022-2024 Martin Leitner-Ankerl.
	* Mersenne Twister Copyright (C) 1997 - 2002 Makoto Matsumoto and Takuji
		Nishimura, Copyright (C) 2000 - 2003 Richard J. Wagner.

Our build system includes third-party CMake modules (these are not compiled
into STP, but they are distributed with it):
	* GetGitRevisionDescription.cmake Copyright Iowa State University 2009-2010.

For testing purposes we also use (but do not compile STP with):
	* llvm-lit Copyright (c) 2003-2014 University of Illinois at Urbana-Champaign.
	* OutputCheck Copyright (c) 2014, Daniel Liew
	* GoogleTest framework Copyright 2008, Google Inc.


Individual licenses are listed below
================================================================================

Bit::Vector
	This package with all its parts is

	Copyright (c) 1995 - 2004 by Steffen Beyer.
	All rights reserved.

	This package is free software; you can use, modify and redistribute
	it under the same terms as Perl itself, i.e., under the terms of
	the "Artistic License" or the "GNU General Public License".

	The C library at the core of this Perl module can additionally
	be used, modified and redistributed under the terms of the
	"GNU Library General Public License".

	Please refer to the files "Artistic.txt", "GNU_GPL.txt" and
	"GNU_LGPL.txt" in this distribution, respectively, for details!

	[STP note: only the C library at the core of the module is imported, as
	lib/extlib-constbv. The three license files named above are part of the
	original Bit::Vector distribution and are not reproduced here; see
	https://dev.perl.org/licenses/ for the Artistic License and the GNU
	General Public License, and https://www.gnu.org/licenses/lgpl-2.0.html
	for the GNU Library General Public License.]

CVC's SMT-LIB Parser
	\file smtlib.y
	
	Author: Sergey Berezin, Clark Barrett
	
	Created: Apr 30 2005
	
	Copyright (C) 2004 by the Board of Trustees of Leland Stanford
	Junior University and by New York University. 
	
	License to use, copy, modify, sell and/or distribute this software
	and its documentation for any purpose is hereby granted without
	royalty, subject to the terms and conditions defined in the \ref
	LICENSE file provided with this distribution.  In particular:
	
	- The above copyright notice and this permission notice must appear
	in all copies of the software and related documentation.
	
	- THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
	EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.

ABC
	Copyright (c) The Regents of the University of California. All rights reserved.

	Permission is hereby granted, without written agreement and without license or
	royalty fees, to use, copy, modify, and distribute this software and its
	documentation for any purpose, provided that the above copyright notice and
	the following two paragraphs appear in all copies of this software.

	IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
	DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF
	THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
	CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

	THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING,
	BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
	A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS,
	AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE,
	SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.

mimalloc
	MIT License

	Copyright (c) 2018-2025 Microsoft Corporation, Daan Leijen

	Permission is hereby granted, free of charge, to any person obtaining a copy
	of this software and associated documentation files (the "Software"), to deal
	in the Software without restriction, including without limitation the rights
	to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
	copies of the Software, and to permit persons to whom the Software is
	furnished to do so, subject to the following conditions:

	The above copyright notice and this permission notice shall be included in all
	copies or substantial portions of the Software.

	THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
	IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
	FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
	AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
	LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
	OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
	SOFTWARE.

ankerl::unordered_dense
	Licensed under the MIT License <http://opensource.org/licenses/MIT>.
	SPDX-License-Identifier: MIT
	Copyright (c) 2022-2024 Martin Leitner-Ankerl <martin.ankerl@gmail.com>

	Permission is hereby granted, free of charge, to any person obtaining a copy
	of this software and associated documentation files (the "Software"), to deal
	in the Software without restriction, including without limitation the rights
	to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
	copies of the Software, and to permit persons to whom the Software is
	furnished to do so, subject to the following conditions:

	The above copyright notice and this permission notice shall be included in all
	copies or substantial portions of the Software.

	THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
	IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
	FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
	AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
	LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
	OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
	SOFTWARE.

Mersenne Twister
	MersenneTwister.h
	Mersenne Twister random number generator -- a C++ class MTRand
	Based on code by Makoto Matsumoto, Takuji Nishimura, and Shawn Cokus
	Richard J. Wagner  v1.0  15 May 2003  rjwagner@writeme.com

	Copyright (C) 1997 - 2002, Makoto Matsumoto and Takuji Nishimura,
	Copyright (C) 2000 - 2003, Richard J. Wagner
	All rights reserved.

	Redistribution and use in source and binary forms, with or without
	modification, are permitted provided that the following conditions
	are met:

		1. Redistributions of source code must retain the above copyright
			notice, this list of conditions and the following disclaimer.

		2. Redistributions in binary form must reproduce the above copyright
			notice, this list of conditions and the following disclaimer in the
			documentation and/or other materials provided with the distribution.

		3. The names of its contributors may not be used to endorse or promote
			products derived from this software without specific prior written
			permission.

	THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
	"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
	LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
	A PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT OWNER
	OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
	EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
	PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
	PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
	LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
	NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
	SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

	The original code included the following notice:

		When you use this, send an email to: matumoto@math.keio.ac.jp
		with an appropriate reference to your work.

	It would be nice to CC: rjwagner@writeme.com and Cokus@math.washington.edu
	when you write.

GetGitRevisionDescription.cmake (cmake/modules)
	Original Author:
	2009-2010 Ryan Pavlik <rpavlik@iastate.edu> <abiryan@ryand.net>
	Iowa State University HCI Graduate Program/VRAC

	Copyright Iowa State University 2009-2010.
	Distributed under the Boost Software License, Version 1.0.

	Permission is hereby granted, free of charge, to any person or organization
	obtaining a copy of the software and accompanying documentation covered by
	this license (the "Software") to use, reproduce, display, distribute,
	execute, and transmit the Software, and to prepare derivative works of the
	Software, and to permit third-parties to whom the Software is furnished to
	do so, all subject to the following:

	The copyright notices in the Software and this entire statement, including
	the above license grant, this restriction and the following disclaimer,
	must be included in all copies of the Software, in whole or in part, and
	all derivative works of the Software, unless such copies or derivative
	works are solely in the form of machine-executable object code generated by
	a source language processor.

	THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
	IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
	FITNESS FOR A PARTICULAR PURPOSE, TITLE AND NON-INFRINGEMENT. IN NO EVENT
	SHALL THE COPYRIGHT HOLDERS OR ANYONE DISTRIBUTING THE SOFTWARE BE LIABLE
	FOR ANY DAMAGES OR OTHER LIABILITY, WHETHER IN CONTRACT, TORT OR OTHERWISE,
	ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
	DEALINGS IN THE SOFTWARE.

LLVM integration tester (llvm-lit)
	University of Illinois/NCSA
	Open Source License

	Copyright (c) 2003-2014 University of Illinois at Urbana-Champaign.
	All rights reserved.

	Developed by:

		LLVM Team

		University of Illinois at Urbana-Champaign

		http://llvm.org

	Permission is hereby granted, free of charge, to any person obtaining a copy of
	this software and associated documentation files (the "Software"), to deal with
	the Software without restriction, including without limitation the rights to
	use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
	of the Software, and to permit persons to whom the Software is furnished to do
	so, subject to the following conditions:

		* Redistributions of source code must retain the above copyright notice,
			this list of conditions and the following disclaimers.

		* Redistributions in binary form must reproduce the above copyright notice,
			this list of conditions and the following disclaimers in the
			documentation and/or other materials provided with the distribution.

		* Neither the names of the LLVM Team, University of Illinois at
			Urbana-Champaign, nor the names of its contributors may be used to
			endorse or promote products derived from this Software without specific
			prior written permission.

	THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
	IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
	FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
	CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
	LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
	OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH THE
	SOFTWARE.

OutputCheck
	Copyright (c) 2014, Daniel Liew All rights reserved.

	Redistribution and use in source and binary forms, with or without modification,
	are permitted provided that the following conditions are met:

	1. Redistributions of source code must retain the above copyright notice, this
	list of conditions and the following disclaimer.

	2. Redistributions in binary form must reproduce the above copyright notice,
	this list of conditions and the following disclaimer in the documentation and/or
	other materials provided with the distribution.

	3. Neither the name of the copyright holder nor the names of its contributors
	may be used to endorse or promote products derived from this software without
	specific prior written permission.

	THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
	ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
	WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
	DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
	ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
	(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
	LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
	ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
	(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
	SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

GoogleTest framework
	Copyright 2008, Google Inc.
	All rights reserved.

	Redistribution and use in source and binary forms, with or without
	modification, are permitted provided that the following conditions are
	met:

		* Redistributions of source code must retain the above copyright
	notice, this list of conditions and the following disclaimer.
		* Redistributions in binary form must reproduce the above
	copyright notice, this list of conditions and the following disclaimer
	in the documentation and/or other materials provided with the
	distribution.
		* Neither the name of Google Inc. nor the names of its
	contributors may be used to endorse or promote products derived from
	this software without specific prior written permission.

	THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
	"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
	LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
	A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
	OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
	SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
	LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
	DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
	THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
	(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
	OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
