Fix sygus substr static symmetry breaking (#1761)

diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 5c073aa0da5b373f531c855e5fa582ceccc5306f..c8d7bf04d8105171e4c5f2d483a6681bebc6ba9b 100644 (file)
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -555,7 +555,8 @@ bool TermDbSygus::considerConst( const Datatype& pdt, TypeNode tnp, Node c, Kind
         }
       }
     }else if( pk==STRING_SUBSTR ){
-      if( c==one_c ){
+      if (c == one_c && arg == 2)
+      {
         rt.d_req_kind = STRING_CHARAT;
         rt.d_children[0].d_req_type = getArgType( pdt[pc], 0 );
         rt.d_children[1].d_req_type = getArgType( pdt[pc], 1 );