summaryrefslogtreecommitdiff
path: root/src/parser/smt2/Smt2.g
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r--src/parser/smt2/Smt2.g4
1 files changed, 1 insertions, 3 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 9d2392715..0526ba66d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -765,9 +765,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
Command* c = new SetUserAttributeCommand("sygus", sygusVar);
c->setMuted(true);
PARSER_STATE->preemptCommand(c);
- c = new AssertCommand(body);
- PARSER_STATE->preemptCommand(c);
- $cmd = new CheckSatCommand();
+ $cmd = new CheckSynthCommand(body);
}
| c = command { $cmd = c; }
// /* error handling */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback