From 346c85d145f6938ce7dce74e7e7cb855d5a6025a Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 8 Mar 2016 12:10:41 -0600
Subject: Extend synthesis solver to handle single invocation with additional
 universal quantification. Refactor query/check-sat to call one internal
 function in SmtEngine. Make check-synth its own command. Minor work on quant
 ee.

---
 src/parser/smt2/Smt2.g | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'src/parser')

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 */
-- 
cgit v1.2.3