Disallow construction of smt_symbol_indext with empty string

Author: thomasspriggs

src/solvers/smt2_incremental/smt_index.cpp

@@ -55,6 +55,7 @@ std::size_t smt_numeral_indext::value() const
 smt_symbol_indext::smt_symbol_indext(irep_idt identifier)
   : smt_indext{ID_smt_symbol_index}
 {
+  PRECONDITION(!identifier.empty());
   set(ID_identifier, identifier);
 }
 

unit/solvers/smt2_incremental/smt_index.cpp

@@ -11,6 +11,13 @@ TEST_CASE("Test smt_indext.pretty is accessible.", "[core][smt2_incremental]")
   REQUIRE_FALSE(index.pretty().empty());
 }
 
+TEST_CASE("Test smt_symbol_index construction", "[core][smt2_incremental]")
+{
+  const cbmc_invariants_should_throwt invariants_throw;
+  CHECK_NOTHROW(smt_symbol_indext{"foo"});
+  CHECK_THROWS(smt_symbol_indext{""});
+}
+
 TEST_CASE("Test smt_index getters", "[core][smt2_incremental]")
 {
   SECTION("Numeral")