A bug fix

stanford-centaur · Oct 27, 2023 · 88a943f · 88a943f
1 parent c0c66ae
commit 88a943f
Showing 1 changed file with 2 additions and 8 deletions.
diff --git a/include/solver.h b/include/solver.h
@@ -219,21 +219,15 @@ class AbsSmtSolver
    * @return a value term with Sort sort and value s
    */
 
-  virtual Term make_term(const std::string& s, bool useEscSequences, const Sort & sort) const{
-        throw NotImplementedException("Strings not supported for this solver.");
-
-  }
+  virtual Term make_term(const std::string& s, bool useEscSequences, const Sort & sort) const = 0;
 
   /* Make a string value term
    * @param s is the value
    * @param sort the sort to create
    * @return a value term with Sort sort and value s
    */  
-  virtual Term make_term(const std::wstring& s, const Sort & sort) const{
-        throw NotImplementedException("Strings not supported for this solver.");
-
-  }
 
+  virtual Term make_term(const std::wstring& s, const Sort & sort) const = 0;
 
   /* Make a bit-vector, int, real or (in the future) string value term
    * @param val the numeric value as a string, or a string value