Merge branch 'main' of https://github.com/cvc5/cvc5

yoni206 · Oct 5, 2023 · c926d61 · c926d61
2 parents b653863 + 26308eb
commit c926d61
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git a/docs/theories/bags.rst b/docs/theories/bags.rst
@@ -17,7 +17,7 @@ a `cvc5::Solver solver` object.
 +----------------------+----------------------------------------------+-------------------------------------------------------------------------+
 | Sort                 | ``(Bag <Sort>)``                             | ``solver.mkBagSort(cvc5::Sort elementSort);``                           |
 +----------------------+----------------------------------------------+-------------------------------------------------------------------------+
-| Constants            | ``(declare-const X (Bag String))``            | ``Sort s = solver.mkBagSort(solver.getStringSort());``                 |
+| Constants            | ``(declare-const X (Bag String))``           | ``Sort s = solver.mkBagSort(solver.getStringSort());``                  |
 |                      |                                              |                                                                         |
 |                      |                                              | ``Term X = solver.mkConst(s, "X");``                                    |
 +----------------------+----------------------------------------------+-------------------------------------------------------------------------+

diff --git a/examples/api/cpp/parser.cpp b/examples/api/cpp/parser.cpp
@@ -37,7 +37,8 @@ int main()
   ss << "(declare-fun b () Int)" << std::endl;
   ss << "(declare-fun c () Int)" << std::endl;
   ss << "(assert (> a (+ b c)))" << std::endl;
-  ss << "(check-sat)" << std::endl;
+  ss << "(assert (< a b))" << std::endl;
+  ss << "(assert (> c 0))" << std::endl;
   parser.setStreamInput(modes::InputLanguage::SMT_LIB_2_6, ss, "MyStream");
 
   // get the symbol manager of the parser, used when invoking commands below
@@ -58,4 +59,9 @@ int main()
     cmd.invoke(&slv, sm, std::cout);
   }
   std::cout << "Finished parsing commands" << std::endl;
+
+  // now, check sat with the solver
+  Result r = slv.checkSat();
+  std::cout << "expected: unsat" << std::endl;
+  std::cout << "result: " << r << std::endl;
 }