Merge branch 'master' into updateScriptsupdateScripts

6 files changed, 52 insertions, 22 deletions

diff --git a/AUTHORS b/AUTHORS
index 299d51ce3..073c1c67f 100644
--- a/AUTHORS
+++ b/AUTHORS
@@ -4,13 +4,28 @@ institutions at the time of their contributions (note that some authors have
 had more than one affiliated institution).  See the file COPYING for details on
 the copyright and licensing of CVC4.
 
-The core designers and authors of CVC4 are:
+The developers and authors of CVC4 are:
 
-  Kshitij Bansal, New York University, Google
+Current:
   Haniel Barbosa, The University of Iowa, Universidade Federal de Minas Gerais
   Clark Barrett, New York University, Google, Stanford University
-  Francois Bobot, The University of Iowa, Commissariat a l'Energie Atomique
   Martin Brain, University of Oxford
+  Ahmed Irfan, Stanford University
+  Makai Mann, Stanford University
+  Abdalrhman Mohamed, The University of Iowa
+  Mudathir Mohamed, The University of Iowa
+  Aina Niemetz, Stanford University
+  Andres Noetzli, Stanford University
+  Alex Ozdemir, Stanford University
+  Mathias Preiner, Stanford University
+  Andrew Reynolds, The University of Iowa, EPFL
+  Ying Sheng, Stanford University
+  Cesare Tinelli, The University of Iowa
+  Yoni Zohar, Stanford University
+
+Alumni:
+  Kshitij Bansal, New York University, Google
+  Francois Bobot, The University of Iowa, Commissariat a l'Energie Atomique
   Christopher Conway, New York University, Google
   Morgan Deters, New York University
   Liana Hadarean, New York University, Mentor Graphics Corporation
@@ -19,12 +34,6 @@ The core designers and authors of CVC4 are:
   Tim King, New York University, Universite Joseph Fourier, Google
   Tianyi Liang, The University of Iowa
   Paul Meng, The University of Iowa
-  Aina Niemetz, Stanford University
-  Andres Noetzli, Stanford University
-  Mathias Preiner, Stanford University
-  Andrew Reynolds, The University of Iowa, EPFL
-  Cesare Tinelli, The University of Iowa
-  Yoni Zohar, Stanford University
 
 Other contributors to the CVC4 codebase are listed in the THANKS file.
 
@@ -36,9 +45,3 @@ CVC4 contains MiniSAT code by Niklas Een and Niklas Sorensson.
 
 The CVC4 parser incorporates some code from ANTLR3, by Jim Idle, Temporal
 Wave LLC.
-
-CVC4 contains various autoconf modules in the config directory. Please refer to
-the individual files for more information on the authors.
-
-CVC4 maintainer versions contain the script autogen.sh by Christopher Sean
-Morrison, and copyright U.S. Army Research Laboratory.
diff --git a/THANKS b/THANKS
index 8eb19e8db..4060d51ef 100644
--- a/THANKS
+++ b/THANKS
@@ -13,6 +13,8 @@ Thanks to:
   College London, headed by Alastair Donaldson) for developing and submitting a
   number of patches in September 2012 related to SMT-LIBv2 compliance.
 
+- Simon Dierl for fixing the ENABLE_BEST option in the build system in 2019.
+
 - Finn Haedicke of University of Bremen, Germany for fixing namespace specifiers
   in CVC4's version of minisat in 2015.
 
@@ -21,8 +23,11 @@ Thanks to:
 - Thomas Hunger for some important patches to CVC4's SWIG interfaces in March
   2014.
 
-- Makai Mann of Stanford University for updating the build scripts to support
-  computing coverage in 2017.
+- Andrew V. Jones for several fixes in 2019 and 2020.
+
+- Mark Laws for fixes in the test suite for Windows in 2017.
+
+- Ken Matsui for fixing compiler warnings in 2019.
 
 - Cristian Mattarei of Stanford University for fixing an issue with parsing
   floating point numbers in 2017.
@@ -33,8 +38,19 @@ Thanks to:
 - Clement Pit-Claudel of MIT for improving the signal handling support for
   Windows builds in 2017.
 
+- Florian Schanda for improving the readability of output of get-model in 2018.
+
+- Tom Smeding for a fix in the contrib/get-antlr-3.4 script in 2018.
+
+- Piotr Troja for several fixes in 2019.
+
 - Arjun Viswanathan for improvements in the CVC and the SMT2 parser.
 
+- Amalee Wilson for a modification of our branch-and-bound method in the linear
+  integer solver to generate ternary clauses instead of binary clauses in 2020.
+  The new method is inspired by the Unit-Cube Tests of Bromberger and Weidenbach
+  at IJCAR'2016.
+
 - Fabian Wolff in 2016 for fixing several spelling mistakes.
 
 - Justin Xu for contributing to refactoring CVC4's preprocessing infrastructure.
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index aed835f3f..a1fd01c96 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -114,7 +114,7 @@ std::string Configuration::getVersionExtra() {
 
 std::string Configuration::copyright() {
   std::stringstream ss;
-  ss << "Copyright (c) 2009-2019 by the authors and their institutional\n"
+  ss << "Copyright (c) 2009-2020 by the authors and their institutional\n"
      << "affiliations listed at http://cvc4.cs.stanford.edu/authors\n\n";
 
   if (Configuration::licenseIsGpl()) {
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 8a2c58b99..7cf6a79bd 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -577,10 +577,9 @@ void UnconstrainedSimplifier::processUnconstrained()
             {
               currentSub = current;
             }
-            if (parent.getType() != current.getType())
-            {
-              currentSub = newUnconstrainedVar(parent.getType(), currentSub);
-            }
+            // always introduce a new variable; it is unsound to try to reuse
+            // currentSub as the variable, see issue #4469.
+            currentSub = newUnconstrainedVar(parent.getType(), currentSub);
             current = parent;
           }
           else
@@ -779,6 +778,10 @@ void UnconstrainedSimplifier::processUnconstrained()
     }
     if (!currentSub.isNull())
     {
+      Trace("unc-simp")
+          << "UnconstrainedSimplifier::processUnconstrained: introduce "
+          << currentSub << " for " << current << ", parent " << parent
+          << std::endl;
       Assert(currentSub.isVar());
       d_substitutions.addSubstitution(current, currentSub, false);
     }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 97a521028..b8304f722 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -552,6 +552,7 @@ set(regress_0_tests
   regress0/issue1063-overloading-dt-sel.smt2
   regress0/issue2832-qualId.smt2
   regress0/issue4010-sort-inf-var.smt2
+  regress0/issue4469-unc-no-reuse-var.smt2
   regress0/ite.cvc
   regress0/ite2.smt2
   regress0/ite3.smt2
diff --git a/test/regress/regress0/issue4469-unc-no-reuse-var.smt2 b/test/regress/regress0/issue4469-unc-no-reuse-var.smt2
new file mode 100644
index 000000000..3bc79578f
--- /dev/null
+++ b/test/regress/regress0/issue4469-unc-no-reuse-var.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --unconstrained-simp --no-check-models
+; EXPECT: sat
+(set-logic QF_AUFBVLIA)
+(declare-fun a () Int)
+(declare-fun b (Int) Int)
+(assert (distinct (b a) (b (b a))))
+(check-sat)