summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus_grammar_cons.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus_grammar_cons.cpp')
-rw-r--r--src/theory/quantifiers/sygus_grammar_cons.cpp3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus_grammar_cons.cpp
index d6a62826f..092880047 100644
--- a/src/theory/quantifiers/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus_grammar_cons.cpp
@@ -580,7 +580,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
cargs.back().push_back(unres_types[i]);
cargs.back().push_back(unres_types[i]);
//type specific predicates
- if( types[i].isInteger() ){
+ if (types[i].isReal())
+ {
CVC4::Kind k = kind::LEQ;
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr());
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback