Commit e38afe6c authored by Fabian Wolff's avatar Fabian Wolff

Add debian/*

parent 9f1db7ed
cvc4 (1.5~pre-20170316) UNRELEASED; urgency=medium
* Initial release. (Closes: #757048)
-- Fabian Wolff <fabi.wolff@arcor.de> Thu, 16 Mar 2017 17:18:54 +0100
Source: cvc4
Maintainer: Fabian Wolff <fabi.wolff@arcor.de>
Section: math
Priority: optional
Build-Depends: debhelper (>= 9),
dh-autoreconf,
libgmp-dev,
libantlr3c-dev,
libboost-thread-dev,
libreadline-dev,
pkg-config,
cxxtest,
chrpath
Standards-Version: 3.9.8
Homepage: http://cvc4.cs.stanford.edu/web/
Package: cvc4
Architecture: any
Depends: libcvc4-3 (= ${binary:Version}),
libcvc4parser3 (= ${binary:Version}),
${shlibs:Depends},
${misc:Depends}
Description: automated theorem prover for SMT problems
CVC4 is an efficient automatic theorem prover for satisfiability
modulo theories (SMT) problems. It can be used to prove the validity
(or, dually, the satisfiability) of first-order formulas in a large
number of built-in logical theories and their combination.
.
CVC4 is intended to be an open and extensible SMT engine, and it can
be used as a stand-alone tool or as a library. It is the fourth in
the Cooperating Validity Checker family of tools (also including CVC,
CVC Lite and CVC3). CVC4 has been designed to increase the
performance and reduce the memory overhead of its predecessors.
.
This package contains binaries needed to use CVC4 as a stand-alone
tool.
Package: libcvc4-dev
Architecture: any
Section: libdevel
Depends: libcvc4-3 (= ${binary:Version}),
libcvc4parser3 (= ${binary:Version}),
${shlibs:Depends},
${misc:Depends}
Description: automated theorem prover for SMT problems (development files)
CVC4 is an efficient automatic theorem prover for satisfiability
modulo theories (SMT) problems. It can be used to prove the validity
(or, dually, the satisfiability) of first-order formulas in a large
number of built-in logical theories and their combination.
.
CVC4 is intended to be an open and extensible SMT engine, and it can
be used as a stand-alone tool or as a library. It is the fourth in
the Cooperating Validity Checker family of tools (also including CVC,
CVC Lite and CVC3). CVC4 has been designed to increase the
performance and reduce the memory overhead of its predecessors.
.
This package contains development files for CVC4. Install it if you
want to develop applications that use CVC4's API.
Package: libcvc4-3
Architecture: any
Section: libs
Depends: ${shlibs:Depends},
${misc:Depends}
Description: automated theorem prover for SMT problems (runtime)
CVC4 is an efficient automatic theorem prover for satisfiability
modulo theories (SMT) problems. It can be used to prove the validity
(or, dually, the satisfiability) of first-order formulas in a large
number of built-in logical theories and their combination.
.
CVC4 is intended to be an open and extensible SMT engine, and it can
be used as a stand-alone tool or as a library. It is the fourth in
the Cooperating Validity Checker family of tools (also including CVC,
CVC Lite and CVC3). CVC4 has been designed to increase the
performance and reduce the memory overhead of its predecessors.
.
This package contains CVC4's runtime shared libraries.
Package: libcvc4parser3
Architecture: any
Section: libs
Depends: ${shlibs:Depends},
${misc:Depends}
Description: automated theorem prover for SMT problems (parser runtime)
CVC4 is an efficient automatic theorem prover for satisfiability
modulo theories (SMT) problems. It can be used to prove the validity
(or, dually, the satisfiability) of first-order formulas in a large
number of built-in logical theories and their combination.
.
CVC4 is intended to be an open and extensible SMT engine, and it can
be used as a stand-alone tool or as a library. It is the fourth in
the Cooperating Validity Checker family of tools (also including CVC,
CVC Lite and CVC3). CVC4 has been designed to increase the
performance and reduce the memory overhead of its predecessors.
.
This package contains runtime shared libraries for CVC4's parser.
Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
Upstream-Name: CVC4
Source: http://cvc4.cs.stanford.edu/downloads/builds/src/
Files: *
Copyright: 2009-2017 New York University and The University of Iowa
License: GPL-3+
Comment: CVC4 is available under both the BSD-3-clause and the
GPL-3+ licenses. For optimal performance, linking against
GPL libraries is recommended, which is why this package is
built and linked against those libraries, resulting in CVC4
being covered by the GPL-3+ license.
Files: debian/*
Copyright: 2017 Fabian Wolff <fabi.wolff@arcor.de>
License: GPL-3+
License: GPL-3+
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or (at
your option) any later version.
.
This program is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
General Public License for more details.
.
You should have received a copy of the GNU General Public License
along with this program. If not, see <http://www.gnu.org/licenses/>.
.
On Debian systems, the complete text of the GNU General Public License
version 3 can be found in the file `/usr/share/common-licenses/GPL-3'.
Files: config/boost.m4
Copyright: 2007-2011 Benoit Sigoure <tsuna@lrde.epita.fr>
License: GPL-3+ with Autoconf exception #1
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or (at
your option) any later version.
.
Additional permission under section 7 of the GNU General Public
License, version 3 ("GPLv3"):
.
If you convey this file as part of a work that contains a
configuration script generated by Autoconf, you may do so under terms
of your choice.
.
This program is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
General Public License for more details.
.
You should have received a copy of the GNU General Public License
along with this program. If not, see <http://www.gnu.org/licenses/>.
.
On Debian systems, the complete text of the GNU General Public License
version 3 can be found in the file `/usr/share/common-licenses/GPL-3'.
Files: config/doxygen.am
Copyright: 2004 Oren Ben-Kiki
License: GPL-3+ with Autoconf exception #2
Files: config/ax_tls.m4
Copyright: 2008 Alan Woodland <ajw05@aber.ac.uk>
2010 Diego Elio Pettenò <flameeyes@gmail.com>
License: GPL-3+ with Autoconf exception #2
License: GPL-3+ with Autoconf exception #2
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or (at
your option) any later version.
.
This program is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
General Public License for more details.
.
You should have received a copy of the GNU General Public License
along with this program. If not, see <http://www.gnu.org/licenses/>.
.
As a special exception, the respective Autoconf Macro's copyright
owner gives unlimited permission to copy, distribute and modify the
configure scripts that are the output of Autoconf when processing the
Macro. You need not follow the terms of the GNU General Public
License when using or distributing such scripts, even though portions
of the text of the Macro appear in them. The GNU General Public
License (GPL) does govern all other use of the material that
constitutes the Autoconf Macro.
.
This special exception to the GPL applies to versions of the Autoconf
Macro released by the Autoconf Archive. When you make and distribute
a modified version of the Autoconf Macro, you may extend this special
exception to the GPL you apply to your modified version as well.
.
On Debian systems, the complete text of the GNU General Public License
version 3 can be found in the file `/usr/share/common-licenses/GPL-3'.
Files: config/pkg.m4
Copyright: 2004 Scott James Remnant <scott@netsplit.com>
License: GPL-3+ with Autoconf exception #3
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or (at
your option) any later version.
.
This program is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
General Public License for more details.
.
You should have received a copy of the GNU General Public License
along with this program. If not, see <http://www.gnu.org/licenses/>.
.
As a special exception to the GNU General Public License, if you
distribute this file as part of a program that contains a
configuration script generated by Autoconf, you may include it under
the same distribution terms that you use for the rest of that
program.
.
On Debian systems, the complete text of the GNU General Public License
version 3 can be found in the file `/usr/share/common-licenses/GPL-3'.
Files: src/parser/bounded_token_buffer.*
src/parser/antlr_input_imports.cpp
Copyright: 2005-2009 Jim Idle, Temporal Wave LLC
License: BSD-3-clause
Files: proofs/lfsc_checker/*
Copyright: 2012-2013 The University of Iowa
License: BSD-3-clause
License: BSD-3-clause
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 name of the author may not be used to endorse or promote products
derived from this software without specific prior written permission.
.
THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``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 AUTHOR 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.
Files: src/util/channel.h
Copyright: 2009-2014 New York University and The University of Iowa
2003-2008 Jan Gaspar
License: BSL-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.
Files: src/prop/minisat/*
src/prop/bvminisat/*
Copyright: 2003-2010 Niklas Sorensson
2003-2006 Niklas Een
License: Expat
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.
usr/bin/cvc4
usr/bin/pcvc4
usr/share/man/man1/cvc4.1
usr/share/man/man1/pcvc4.1
usr/lib/*/libcvc4.so.*
usr/include/cvc4
usr/lib/*/*.a
usr/lib/*/*.so
usr/lib/*/libcvc4parser.so.*
Description: Fix a compilation error
Author: Fabian Wolff <fabi.wolff@arcor.de>
Forwarded: no
Last-Update: 2017-03-17
---
This patch header follows DEP-3: http://dep.debian.net/deps/dep3/
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -104,7 +104,7 @@
}
#if HAVE_LIBREADLINE
- if(d_in == cin) {
+ if(&d_in == &cin) {
::rl_readline_name = const_cast<char*>("CVC4");
#if READLINE_COMPENTRY_FUNC_RETURNS_CHARP
::rl_completion_entry_function = commandGenerator;
Description: Make timestamps reproducible
Author: Fabian Wolff <fabi.wolff@arcor.de>
Forwarded: no
Last-Update: 2017-03-17
---
This patch header follows DEP-3: http://dep.debian.net/deps/dep3/
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -291,7 +291,7 @@
}
std::string Configuration::getCompiledDateTime() {
- return __DATE__ " " __TIME__;
+ return DEB_BUILD_DATE " " DEB_BUILD_TIME;
}
}/* CVC4 namespace */
Description: Remove erroneous include path
Author: Fabian Wolff <fabi.wolff@arcor.de>
Forwarded: no
Last-Update: 2017-03-17
---
This patch header follows DEP-3: http://dep.debian.net/deps/dep3/
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -69,7 +69,6 @@
AM_CPPFLAGS = \
-I. \
- "-I@CXXTEST@" \
"-I@top_builddir@/src" \
"-I@top_srcdir@/src/include" \
"-I@top_srcdir@/lib" \
Description: Fix spelling errors found by Lintian
Author: Fabian Wolff <fabi.wolff@arcor.de>
Forwarded: no
Last-Update: 2017-03-17
---
This patch header follows DEP-3: http://dep.debian.net/deps/dep3/
--- a/doc/cvc4.1
+++ b/doc/cvc4.1
@@ -176,7 +176,7 @@
.IP "\-\-replay\-reject\-cut"
maximum complexity of any coefficient while replaying cuts
.IP "\-\-replay\-lemma\-reject\-cut"
-maximum complexity of any coefficient while outputing replaying cut lemmas
+maximum complexity of any coefficient while outputting replaying cut lemmas
.IP "\-\-replay\-soi\-major\-threshold"
threshold for a major tolerance failure by the approximate solver
.IP "\-\-replay\-soi\-major\-threshold\-pen"
@@ -784,38 +784,38 @@
.IP "\-\-model\-u\-dt\-enum"
in models, output uninterpreted sorts as datatype enumerations [*]
.IP "\-\-rewrite\-step"
-ammount of resources spent for each rewrite step (EXPERTS only)
+amount of resources spent for each rewrite step (EXPERTS only)
.IP "\-\-theory\-check\-step"
-ammount of resources spent for each theory check call (EXPERTS only)
+amount of resources spent for each theory check call (EXPERTS only)
.IP "\-\-decision\-step"
-ammount of getNext decision calls in the decision engine (EXPERTS only)
+amount of getNext decision calls in the decision engine (EXPERTS only)
.IP "\-\-bitblast\-step"
-ammount of resources spent for each bitblast step (EXPERTS only)
+amount of resources spent for each bitblast step (EXPERTS only)
.IP "\-\-parse\-step"
-ammount of resources spent for each command/expression parsing (EXPERTS only)
+amount of resources spent for each command/expression parsing (EXPERTS only)
.IP "\-\-lemma\-step"
-ammount of resources spent when adding lemmas (EXPERTS only)
+amount of resources spent when adding lemmas (EXPERTS only)
.IP "\-\-restart\-step"
-ammount of resources spent for each theory restart (EXPERTS only)
+amount of resources spent for each theory restart (EXPERTS only)
.IP "\-\-cnf\-step"
-ammount of resources spent for each call to cnf conversion (EXPERTS only)
+amount of resources spent for each call to cnf conversion (EXPERTS only)
.IP "\-\-preprocess\-step"
-ammount of resources spent for each preprocessing step in SmtEngine (EXPERTS only)
+amount of resources spent for each preprocessing step in SmtEngine (EXPERTS only)
.IP "\-\-quantifier\-step"
-ammount of resources spent for quantifier instantiations (EXPERTS only)
+amount of resources spent for quantifier instantiations (EXPERTS only)
.IP "\-\-sat\-conflict\-step"
-ammount of resources spent for each sat conflict (main sat solver) (EXPERTS only)
+amount of resources spent for each sat conflict (main sat solver) (EXPERTS only)
.IP "\-\-bv\-sat\-conflict\-step"
-ammount of resources spent for each sat conflict (bitvectors) (EXPERTS only)
+amount of resources spent for each sat conflict (bitvectors) (EXPERTS only)
.IP "\-\-rewrite\-apply\-to\-const"
--- a/proofs/signatures/signatures.cpp
+++ b/proofs/signatures/signatures.cpp
@@ -1359,7 +1359,7 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\n\
\n\
; bit blast x = y\n\
-; for x,y of size n, it will return a conjuction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1})))\n\
+; for x,y of size n, it will return a conjunction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1})))\n\
; f is the accumulator formula that builds the equality in the right order\n\
(program bblast_eq_rec ((x bblt) (y bblt) (f formula)) formula\n\
(match x\n\
--- a/proofs/signatures/th_bv_bitblast.plf
+++ b/proofs/signatures/th_bv_bitblast.plf
@@ -425,7 +425,7 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; bit blast x = y
-; for x,y of size n, it will return a conjuction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1})))
+; for x,y of size n, it will return a conjunction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1})))
; f is the accumulator formula that builds the equality in the right order
(program bblast_eq_rec ((x bblt) (y bblt) (f formula)) formula
(match x
--- a/src/options/arith_options
+++ b/src/options/arith_options
@@ -135,7 +135,7 @@
maximum complexity of any coefficient while replaying cuts
option lemmaRejectCutSize --replay-lemma-reject-cut unsigned :default 25500
- maximum complexity of any coefficient while outputing replaying cut lemmas
+ maximum complexity of any coefficient while outputting replaying cut lemmas
option soiApproxMajorFailure --replay-soi-major-threshold double :default .01
threshold for a major tolerance failure by the approximate solver
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -958,7 +958,7 @@
Bit-blasting modes currently supported by the --bitblast option:\n\
\n\
lazy (default)\n\
-+ Separate boolean structure and term reasoning betwen the core\n\
++ Separate boolean structure and term reasoning between the core\n\
SAT solver and the bv SAT solver\n\
\n\
eager\n\
--- a/src/options/smt_options
+++ b/src/options/smt_options
@@ -108,40 +108,40 @@
# Resource spending options for SPARK
expert-option rewriteStep rewrite-step --rewrite-step unsigned :default 1
- ammount of resources spent for each rewrite step
+ amount of resources spent for each rewrite step
expert-option theoryCheckStep theory-check-step --theory-check-step unsigned :default 1
- ammount of resources spent for each theory check call
+ amount of resources spent for each theory check call
expert-option decisionStep decision-step --decision-step unsigned :default 1
- ammount of getNext decision calls in the decision engine
+ amount of getNext decision calls in the decision engine
expert-option bitblastStep bitblast-step --bitblast-step unsigned :default 1
- ammount of resources spent for each bitblast step
+ amount of resources spent for each bitblast step
expert-option parseStep parse-step --parse-step unsigned :default 1
- ammount of resources spent for each command/expression parsing
+ amount of resources spent for each command/expression parsing
expert-option lemmaStep lemma-step --lemma-step unsigned :default 1
- ammount of resources spent when adding lemmas
+ amount of resources spent when adding lemmas
expert-option restartStep restart-step --restart-step unsigned :default 1
- ammount of resources spent for each theory restart
+ amount of resources spent for each theory restart
expert-option cnfStep cnf-step --cnf-step unsigned :default 1
- ammount of resources spent for each call to cnf conversion
+ amount of resources spent for each call to cnf conversion
expert-option preprocessStep preprocess-step --preprocess-step unsigned :default 1
- ammount of resources spent for each preprocessing step in SmtEngine
+ amount of resources spent for each preprocessing step in SmtEngine
expert-option quantifierStep quantifier-step --quantifier-step unsigned :default 1
- ammount of resources spent for quantifier instantiations
+ amount of resources spent for quantifier instantiations
expert-option satConflictStep sat-conflict-step --sat-conflict-step unsigned :default 1
- ammount of resources spent for each sat conflict (main sat solver)
+ amount of resources spent for each sat conflict (main sat solver)
expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step unsigned :default 1
- ammount of resources spent for each sat conflict (bitvectors)
+ amount of resources spent for each sat conflict (bitvectors)
expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -210,7 +210,7 @@
// Todo improve the exception thrown
std::stringstream ss;
ss << "The POW(^) operator can only be used with a natural number ";
- ss << "in the exponent. Exception occured in:" << std::endl;
+ ss << "in the exponent. Exception occurred in:" << std::endl;
ss << " " << t;
throw LogicException(ss.str());
}
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -302,7 +302,7 @@
operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body"
-parameterized CHAIN CHAIN_OP 2: "chained operator (N-ary), turned into a conjuction of binary applications of the operator on adjoining parameters; first parameter is a CHAIN_OP representing a binary operator, rest are arguments to that operator"
+parameterized CHAIN CHAIN_OP 2: "chained operator (N-ary), turned into a conjunction of binary applications of the operator on adjoining parameters; first parameter is a CHAIN_OP representing a binary operator, rest are arguments to that operator"
constant CHAIN_OP \
::CVC4::Chain \
::CVC4::ChainHashFunction \
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -98,7 +98,7 @@
if( check ) {
TypeNode t = n[0].getType(check);
if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(n, "expecting an orginal string term in string contain");
+ throw TypeCheckingExceptionPrivate(n, "expecting an original string term in string contain");
}
t = n[1].getType(check);
if (!t.isString()) {
--- a/test/regress/regress0/arith/bug716.1.cvc
+++ b/test/regress/regress0/arith/bug716.1.cvc
@@ -1,4 +1,4 @@
-% EXPECT: The POW(^) operator can only be used with a natural number in the exponent. Exception occured in:
+% EXPECT: The POW(^) operator can only be used with a natural number in the exponent. Exception occurred in:
% EXPECT: 2 ^ x
% EXIT: 1
x: INT;
01-ref-compare.patch
02-timestamps.patch
03-include-paths.patch
04-spelling-errors.patch
#!/usr/bin/make -f
# Uncomment this to turn on verbose mode.
# export DH_VERBOSE=1
export DEB_BUILD_MAINT_OPTIONS = hardening=+all
export DEB_CPPFLAGS_MAINT_APPEND = \
-DDEB_BUILD_DATE="\"$(shell dpkg-parsechangelog -SDate | date -f- +%F)\"" \
-DDEB_BUILD_TIME="\"$(shell dpkg-parsechangelog -SDate | date -f- +%T)\""
%:
dh $@ --parallel --with autoreconf
override_dh_auto_configure:
dh_auto_configure -- --enable-static --enable-shared \
--with-build=production --enable-gpl --with-portfolio \
--enable-unit-testing --with-readline --without-compat
override_dh_install:
chrpath -d debian/tmp/usr/bin/pcvc4
dh_install
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment