Merge branch '1.4.x'

Conflicts:
	NEWS

diff --cc NEWS
index 84debe315f92ee589bdad2e9d43e26a2e660de18,4c0de2ce30a02837c2a00435a2e81c61d16c9ea7..7e3a30d742cc580254c05ae4b6357f8595973835
--- 1/NEWS
--- 2/NEWS
+++ b/NEWS
@@@ -3,10 -3,8 +3,12 @@@ This file contains a summary of importa
  Changes since 1.4
  =================
  
 +* Support for unsat cores.
 +* Simplification mode "incremental" no longer supported.
 +* Support for array constants in constraints.
 +* Syntax for array models have changed in some language front-ends.
+ * In SMT-LIB model output, real-sorted but integer-valued constants are
+   now printed in accordance with the standard (e.g. "1.0").
  
  Changes since 1.3
  =================

diff --cc src/expr/command.cpp
Simple merge

diff --cc src/parser/cvc/Cvc.g
Simple merge

diff --cc src/printer/cvc/cvc_printer.cpp
index 2d89d3affcc25d12fa39cb6616e337dba1525e0e,3f93106a029c54690454b3644d7d687598866a7e..ed5116bc626f66e07c6e553b1cf460ccae7ccc94
--- 1/src/printer/cvc/cvc_printer.cpp
--- 2/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@@ -162,22 -165,13 +165,20 @@@ void CvcPrinter::toStream(std::ostream
        out << n.getConst<Datatype>().getName();
        break;
  
-     case kind::EMPTYSET: {
+     case kind::EMPTYSET:
        out << "{} :: " << n.getConst<EmptySet>().getType();
-       return;
        break;
-     }
  
 +    case kind::STORE_ALL: {
 +      const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>();
 +      out << "ARRAY(" << asa.getType().getIndexType() << " OF "
 +          << asa.getType().getConstituentType() << ") : " << asa.getExpr();
 +      break;
 +    }
 +
      default:
-       // fall back on whatever operator<< does on underlying type; we
-       // might luck out and print something reasonable
+       // Fall back to whatever operator<< does on underlying type; we
+       // might luck out and print something reasonable.
        kind::metakind::NodeValueConstPrinter::toStream(out, n);
      }
  

diff --cc src/printer/smt2/smt2_printer.cpp
Simple merge