From eab2dae9d14e54ead1100e07b41c4af8e1b41368 Mon Sep 17 00:00:00 2001
From: Bruno Andreotti <bandreotti@proton.me>
Date: Mon, 23 Oct 2023 13:18:45 -0300
Subject: [PATCH] Add support for `check-sat-assuming` command

---
 carcara/src/parser/lexer.rs | 4 ++++
 carcara/src/parser/mod.rs   | 6 ++++++
 2 files changed, 10 insertions(+)

diff --git a/carcara/src/parser/lexer.rs b/carcara/src/parser/lexer.rs
index 3ec929d3..3f18e7df 100644
--- a/carcara/src/parser/lexer.rs
+++ b/carcara/src/parser/lexer.rs
@@ -102,6 +102,9 @@ pub enum Reserved {
     /// The `assert` reserved word.
     Assert,
 
+    /// The `check-sat-assuming` reserved word.
+    CheckSatAssuming,
+
     /// The `set-logic` reserved word.
     SetLogic,
 }
@@ -125,6 +128,7 @@ impl_str_conversion_traits!(Reserved {
     DeclareSort: "declare-sort",
     DefineFun: "define-fun",
     Assert: "assert",
+    CheckSatAssuming: "check-sat-assuming",
     SetLogic: "set-logic",
 });
 
diff --git a/carcara/src/parser/mod.rs b/carcara/src/parser/mod.rs
index e4f240a6..807acf8c 100644
--- a/carcara/src/parser/mod.rs
+++ b/carcara/src/parser/mod.rs
@@ -551,6 +551,12 @@ impl<'a, R: BufRead> Parser<'a, R> {
                     self.expect_token(Token::CloseParen)?;
                     self.premises().insert(term);
                 }
+                Token::ReservedWord(Reserved::CheckSatAssuming) => {
+                    self.expect_token(Token::OpenParen)?;
+                    let terms = self.parse_sequence(Self::parse_term, true)?;
+                    self.expect_token(Token::CloseParen)?;
+                    self.premises().extend(terms);
+                }
                 Token::ReservedWord(Reserved::SetLogic) => {
                     let logic = self.expect_symbol()?;
                     self.expect_token(Token::CloseParen)?;