summaryrefslogtreecommitdiff
path: root/src/parser/smt2/smt2.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2/smt2.h')
-rw-r--r--src/parser/smt2/smt2.h8
1 files changed, 4 insertions, 4 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 35ac781f5..53ebf5929 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -602,10 +602,10 @@ class Smt2 : public Parser
* by a lambda), and cargs contains the types of the arguments of the
* sygus constructor.
*/
- Expr purifySygusGTerm(Expr term,
- std::map<Expr, Type>& ntsToUnres,
- std::vector<Expr>& args,
- std::vector<Type>& cargs) const;
+ api::Term purifySygusGTerm(api::Term term,
+ std::map<Expr, Type>& ntsToUnres,
+ std::vector<api::Term>& args,
+ std::vector<api::Sort>& cargs) const;
void addArithmeticOperators();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback