summaryrefslogtreecommitdiff
path: root/src/parser/smt2
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2')
-rw-r--r--src/parser/smt2/smt2.cpp6
1 files changed, 1 insertions, 5 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index cc3b09cfe..7e621f56b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -545,11 +545,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
std::map< Type, std::vector< DatatypeConstructorArg > > sels;
//types for each of the variables
for( unsigned i=0; i<sygus_vars.size(); i++ ){
- Type t = sygus_vars[i].getType();
- if( !t.isBoolean() && std::find( types.begin(), types.end(), t )==types.end() ){
- Debug("parser-sygus") << "...will make grammar for " << t << std::endl;
- types.push_back( t );
- }
+ collectSygusGrammarTypesFor( sygus_vars[i].getType(), types, sels );
}
//types connected to range
collectSygusGrammarTypesFor( range, types, sels );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback