7 files changed, 91 insertions, 2 deletions
diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index c4e670f6d..9a6d880e9 100644
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -53,6 +53,7 @@ std::unordered_map<std::string, Smt1::Logic> Smt1::newLogicMap() {
   logicMap["QF_UFNIRA"] = QF_UFNIRA;
   logicMap["QF_AUFLIA"] = QF_AUFLIA;
   logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
+  logicMap["SAT"] = SAT;
   logicMap["UFNIA"] = UFNIA;
   logicMap["UFNIRA"] = UFNIRA;
   logicMap["UFLRA"] = UFLRA;
@@ -205,6 +206,9 @@ void Smt1::setLogic(const std::string& name) {
   case QF_SAT:
     /* no extra symbols needed */
     break;
+  case SAT:
+    addTheory(THEORY_QUANTIFIERS);
+    break;
 
   case QF_UFIDL:
   case QF_UFLIA:
diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h
index e9dbea1a9..036453675 100644
--- a/src/parser/smt1/smt1.h
+++ b/src/parser/smt1/smt1.h
@@ -62,6 +62,7 @@ public:
     QF_UFLIRA, // nonstandard
     QF_UFNIRA, // nonstandard
     QF_UFNRA,
+    SAT,
     UFLRA,
     UFNIRA, // nonstandard
     UFNIA,
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index ad3a010c0..335a87501 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -336,6 +336,10 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
   } else if(!strcmp(p, "QF_SAT")) {
     // propositional logic only; we're done.
     p += 6;
+  } else if(!strcmp(p, "SAT")) {
+    // quantified Boolean formulas only; we're done.
+    enableQuantifiers();
+    p += 3;
   } else if(!strcmp(p, "QF_ALL_SUPPORTED")) {
     // the "all theories included" logic, no quantifiers
     enableEverything();
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index b2ed657d0..122f9219b 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -78,7 +78,8 @@ TESTS =	\
 	cruanes-no-minimal-unk.smt2 \
 	no-minimal-sat.smt2 \
 	issue916-fmf-or.smt2 \
-	pow2-bool.smt2 
+	pow2-bool.smt2 \
+	sat-logic.smt2 
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/sat-logic.smt2 b/test/regress/regress0/fmf/sat-logic.smt2
new file mode 100644
index 000000000..678ea3079
--- /dev/null
+++ b/test/regress/regress0/fmf/sat-logic.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic SAT)
+(set-info :status sat)
+(assert (forall ((x Bool) (y Bool)) (exists ((z Bool)) (= z (and x y)))))
+(check-sat)
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 6dfcb922a..3c118a007 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -66,7 +66,8 @@ TESTS = commutative.sy \
         cegar1.sy \
         triv-type-mismatch-si.sy \
         nia-max-square-ns.sy \
-        strings-concat-3-args.sy
+        strings-concat-3-args.sy \
+        ccp16.lus.sy
 
 
 # sygus tests currently taking too long for make regress
diff --git a/test/regress/regress0/sygus/ccp16.lus.sy b/test/regress/regress0/sygus/ccp16.lus.sy
new file mode 100644
index 000000000..662069105
--- /dev/null
+++ b/test/regress/regress0/sygus/ccp16.lus.sy
@@ -0,0 +1,72 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic SAT)
+
+(define-fun
+  __node_init_top_0 (
+    (top.usr.OK_a_0 Bool)
+    (top.res.init_flag_a_0 Bool)
+  ) Bool
+  
+  (and (= top.usr.OK_a_0 true) top.res.init_flag_a_0)
+)
+
+(define-fun
+  __node_trans_top_0 (
+    (top.usr.OK_a_1 Bool)
+    (top.res.init_flag_a_1 Bool)
+    (top.usr.OK_a_0 Bool)
+    (top.res.init_flag_a_0 Bool)
+  ) Bool
+  
+  (and (= top.usr.OK_a_1 true) (not top.res.init_flag_a_1))
+)
+
+
+
+(synth-inv str_invariant(
+  (top.usr.OK Bool)
+  (top.res.init_flag Bool)
+))
+
+
+(declare-primed-var top.usr.OK Bool)
+(declare-primed-var top.res.init_flag Bool)
+
+(define-fun
+  init (
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+  ) Bool
+  
+  (and (= top.usr.OK true) top.res.init_flag)
+)
+
+(define-fun
+  trans (
+    
+    ;; Current state.
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+    
+    ;; Next state.
+    (top.usr.OK! Bool)
+    (top.res.init_flag! Bool)
+  
+  ) Bool
+  
+  (and (= top.usr.OK! true) (not top.res.init_flag!))
+)
+
+(define-fun
+  prop (
+    (top.usr.OK Bool)
+    (top.res.init_flag Bool)
+  ) Bool
+  
+  top.usr.OK
+)
+
+(inv-constraint str_invariant init trans prop)
+
+(check-synth)