diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-06 09:35:49 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-06 09:35:59 +0100 |
| commit | 363e4c378f0bc9598a93c80bce9ecaebca2efdd1 (patch) | |
| tree | e40a637326719738866bfbb790aa704a3522a2c1 /src/parser/smt2 | |
| parent | fca6fd532abda44c4da48d5c167b77600690e221 (diff) | |
Handle missing cases for single inv solution reconstruction. Minor fixes. Refactor.
Diffstat (limited to 'src/parser/smt2')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 3fa27e474..902e745ea 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -709,6 +709,9 @@ sygusGTerm[std::string& fun, std::vector<CVC4::Expr>& ops, std::vector<std::stri : LPAREN_TOK ( builtinOp[k] { Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl; + if( k==CVC4::kind::BITVECTOR_UDIV ){ + k = CVC4::kind::BITVECTOR_UDIV_TOTAL; + } ops.push_back(EXPR_MANAGER->operatorOf(k)); name = kind::kindToString(k); } |