diff --git a/integration-tests/c-example/lib/input_output/input_output.c b/integration-tests/c-example/lib/input_output/input_output.c
new file mode 100644
index 00000000..bb2fcfcb
--- /dev/null
+++ b/integration-tests/c-example/lib/input_output/input_output.c
@@ -0,0 +1,186 @@
+#include <stdio.h>
+#include "input_output.h"
+
+int simple_getc() {
+    unsigned char a = getc(stdin);
+    if (a == '0') {
+        return 0;
+    } else if (a == '1') {
+        return 1;
+    } else if (a == '2') {
+        return 2;
+    } else if (a == '3') {
+        return 3;
+    } else if (a == '4') {
+        return 4;
+    } else if (a == '5') {
+        return 5;
+    } else if (a == '6') {
+        return 6;
+    } else if (a == '7') {
+        return 7;
+    } else if (a == '8') {
+        return 8;
+    } else if (a == '9') {
+        return 9;
+    }
+    return -1;
+}
+
+int simple_fgetc(int x) {
+    if (x >= 0 && x <= 9) {
+        unsigned char a = fgetc(stdin);
+        if (a >= 'a' && a <= 'z') {
+            return 1;
+        } else {
+            return 2;
+        }
+    } else {
+        unsigned char a = fgetc(stdin);
+        unsigned char b = fgetc(stdin);
+        if (a >= 'a' && a <= 'z') {
+            if (b >= '0' && b <= '9') {
+                return 3;
+            } else {
+                return 4;
+            }
+        } else {
+            return 5;
+        }
+    }
+}
+
+int simple_fread() {
+    int arrA[4];
+    int arrB[4];
+    fread(arrA, sizeof(int), 4, stdin);
+    fread(arrB, sizeof(int), 4, stdin);
+
+    int sumA = 0, sumB = 0;
+    for (int i = 0; i < 4; i++) {
+        sumA += arrA[i];
+        sumB += arrB[i];
+    }
+    if (sumA == sumB) {
+        return 0;
+    } else if (sumA > sumB) {
+        return 1;
+    } else {
+        return -1;
+    }
+}
+
+int simple_fgets() {
+    char a[8];
+    fgets(a, 6, stdin);
+    if (a[0] == 'u' && a[1] == 't' && a[2] == 'b' && a[3] == 'o' && a[4] == 't') {
+        return 1;
+    }
+    return 0;
+}
+
+int simple_getchar() {
+    unsigned char a = getchar();
+    unsigned char b = getchar();
+
+    if (a + b < 0) {
+        return -1;
+    }
+
+    if (a + b < 100) {
+        return 0;
+    } else if (a + b < 200) {
+        return 1;
+    } else {
+        return 2;
+    }
+}
+
+int simple_gets() {
+    char a[8];
+    gets(a);
+    if (a[0] == 'u' && a[1] == 't' && a[2] == 'b' && a[3] == 'o' && a[4] == 't') {
+        return 1;
+    }
+    return 0;
+}
+
+char simple_putc(int x, int y) {
+    if (x + y > 0) {
+        putc('1', stdout);
+        return '1';
+    } else if (x + y < 0) {
+        putc('2', stdout);
+        return '2';
+    } else {
+        putc('0', stdout);
+        return '0';
+    }
+}
+
+char simple_fputc(int x, int y) {
+    if (x < y) {
+        fputc('<', stdout);
+        return '<';
+    } else if (x > y) {
+        fputc('>', stdout);
+        return '>';
+    } else {
+        fputc('=', stdout);
+        return '=';
+    }
+}
+
+char simple_fwrite(int x) {
+    if (x > 0) {
+        char a[] = "Positive";
+        fwrite(a, sizeof(char), 8, stdout);
+        return 'P';
+    } else if (x < 0) {
+        char a[] = "Negative";
+        fwrite(a, sizeof(char), 8, stdout);
+        return 'N';
+    } else {
+        char a[] = "Zero";
+        fwrite(a, sizeof(char), 4, stdout);
+        return 'Z';
+    }
+}
+
+char simple_fputs(char c) {
+    if (c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u') {
+        char a[] = "Vowel";
+        fputs("Vowel", stdout);
+        return 'V';
+    } else {
+        char a[] = "Consonant";
+        fputs("Consonant", stdout);
+        return 'C';
+    }
+}
+
+char simple_putchar(int x, int y) {
+    if (3 * x > 2 * y) {
+        putchar('>');
+        return '>';
+    } else if (3 * x < 2 * y) {
+        putchar('<');
+        return '<';
+    } else {
+        putchar('=');
+        return '=';
+    }
+}
+
+char simple_puts(char c) {
+    if (c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u') {
+        char a[] = "Vowel";
+        puts(a);
+        return 'V';
+    } else {
+        char a[] = "Consonant";
+        puts(a);
+        return 'C';
+    }
+}
+
diff --git a/integration-tests/c-example/lib/input_output/input_output.h b/integration-tests/c-example/lib/input_output/input_output.h
new file mode 100644
index 00000000..40ce5cbc
--- /dev/null
+++ b/integration-tests/c-example/lib/input_output/input_output.h
@@ -0,0 +1,29 @@
+#ifndef INPUT_OUTPUT_H
+#define INPUT_OUTPUT_H
+
+int simple_getc();
+
+int simple_fgetc(int x);
+
+int simple_fread();
+
+int simple_fgets();
+
+int simple_getchar();
+
+int simple_gets();
+
+char simple_putc(int x, int y);
+
+char simple_fputc(int x, int y);
+
+char simple_fwrite(int x);
+
+char simple_fputs(char c);
+
+char simple_putchar(int x, int y);
+
+char simple_puts(char c);
+
+#endif
+
diff --git a/server/src/KleeRunner.cpp b/server/src/KleeRunner.cpp
index 9bc93124..61f7e1b5 100644
--- a/server/src/KleeRunner.cpp
+++ b/server/src/KleeRunner.cpp
@@ -198,6 +198,7 @@ void KleeRunner::processBatchWithoutInteractive(MethodKtests &ktestChunk,
     std::vector<std::string> argvData = { "klee",
                                           entryPointFlag,
                                           "--libc=klee",
+                                          "--utbot",
                                           "--posix-runtime",
                                           "--fp-runtime",
                                           "--only-output-states-covering-new",
@@ -268,6 +269,7 @@ void KleeRunner::processBatchWithInteractive(const std::vector<tests::TestMethod
     std::vector<std::string> argvData = { "klee",
                                           entryPointFlag,
                                           "--libc=klee",
+                                          "--utbot",
                                           "--posix-runtime",
                                           "--fp-runtime",
                                           "--only-output-states-covering-new",
diff --git a/server/src/Tests.cpp b/server/src/Tests.cpp
index 76163dee..1b6b8795 100644
--- a/server/src/Tests.cpp
+++ b/server/src/Tests.cpp
@@ -508,6 +508,7 @@ void KTestObjectParser::parseKTest(const MethodKtests &batch,
                                    bool filterByLineFlag,
                                    std::shared_ptr<LineInfo> lineInfo) {
     LOG_SCOPE_FUNCTION(DEBUG);
+    sourceFilePath = tests.sourceFilePath;
     for (auto &[testMethod, testCases] : batch) {
         auto it = tests.methods.find<std::string, tests::Tests::MethodDescriptionToStringEqual>(
             testMethod.methodName);
@@ -852,9 +853,9 @@ KTestObjectParser::parseTestCaseParams(const UTBotKTest &ktest,
         processGlobalParamPostValue(testCaseDescription, globalParam, rawKleeParams);
     }
 
-    //We should turn off symbolic stdin, because it doesn't work correct with interactive mode
-    //TODO: rewrite symbolic stdin, so that it can work with interactive mode
-    //processSymbolicStdin(testCaseDescription, rawKleeParams);
+    if (Paths::getSourceLanguage(sourceFilePath) == utbot::Language::C) {
+        processSymbolicStdin(testCaseDescription, rawKleeParams);
+    }
 
     processStubParamValue(testCaseDescription, methodNameToReturnTypeMap, rawKleeParams);
     if (!types::TypesHandler::skipTypeInReturn(methodDescription.returnType)) {
diff --git a/server/src/Tests.h b/server/src/Tests.h
index 0b434e88..1a6d2635 100644
--- a/server/src/Tests.h
+++ b/server/src/Tests.h
@@ -569,6 +569,8 @@ namespace tests {
                         bool filterByLineFlag,
                         std::shared_ptr<LineInfo> lineInfo);
     private:
+        fs::path sourceFilePath;
+
         types::TypesHandler &typesHandler;
 
         struct RawKleeParam {
diff --git a/server/src/printers/KleePrinter.cpp b/server/src/printers/KleePrinter.cpp
index 71ca34ac..51267c65 100644
--- a/server/src/printers/KleePrinter.cpp
+++ b/server/src/printers/KleePrinter.cpp
@@ -32,6 +32,45 @@ printer::KleePrinter::KleePrinter(const types::TypesHandler *typesHandler,
     : Printer(srcLanguage), typesHandler(typesHandler), buildDatabase(std::move(buildDatabase)) {
 }
 
+void KleePrinter::writePosixWrapper(const Tests &tests,
+                                    const tests::Tests::MethodDescription &testMethod) {
+    declTestEntryPoint(tests, testMethod, false);
+    strFunctionCall(PrinterUtils::POSIX_INIT, {"&" + PrinterUtils::UTBOT_ARGC, "&" + PrinterUtils::UTBOT_ARGV});
+    std::string entryPoint = KleeUtils::entryPointFunction(tests, testMethod.name, false, true);
+    strDeclareVar("int", KleeUtils::RESULT_VARIABLE_NAME, constrFunctionCall(entryPoint,
+                        {PrinterUtils::UTBOT_ARGC, PrinterUtils::UTBOT_ARGV, PrinterUtils::UTBOT_ENVP},
+                        "", std::nullopt, false));
+    strFunctionCall(PrinterUtils::POSIX_CHECK_STDIN_READ, {});
+    strReturn(KleeUtils::RESULT_VARIABLE_NAME);
+    closeBrackets(1);
+    ss << NL;
+}
+
+void KleePrinter::writeTestedFunction(const Tests &tests,
+                                      const tests::Tests::MethodDescription &testMethod,
+                                      const std::optional<LineInfo::PredicateInfo> &predicateInfo,
+                                      const std::string &testedMethod,
+                                      bool onlyForOneEntity,
+                                      bool isWrapped) {
+    writeStubsForFunctionParams(typesHandler, testMethod, true);
+    declTestEntryPoint(tests, testMethod, isWrapped);
+    genGlobalParamsDeclarations(testMethod);
+    genParamsDeclarations(testMethod);
+    genPostGlobalSymbolicVariables(testMethod);
+    genPostParamsSymbolicVariables(testMethod);
+    if (types::TypesHandler::skipTypeInReturn(testMethod.returnType)) {
+        genVoidFunctionAssumes(testMethod, predicateInfo, testedMethod, onlyForOneEntity);
+    } else {
+        genNonVoidFunctionAssumes(testMethod, predicateInfo, testedMethod,
+                                  onlyForOneEntity);
+    }
+    genGlobalsKleeAssumes(testMethod);
+    genPostParamsKleeAssumes(testMethod);
+    strReturn("0");
+    closeBrackets(1);
+    ss << NL;
+}
+
 fs::path KleePrinter::writeTmpKleeFile(
     const Tests &tests,
     const std::string &buildDir,
@@ -92,22 +131,12 @@ fs::path KleePrinter::writeTmpKleeFile(
             continue;
         }
         try {
-            writeStubsForFunctionParams(typesHandler, testMethod, true);
-            declTestEntryPoint(tests, testMethod);
-            genGlobalParamsDeclarations(testMethod);
-            genParamsDeclarations(testMethod);
-            genPostGlobalSymbolicVariables(testMethod);
-            genPostParamsSymbolicVariables(testMethod);
-            if (types::TypesHandler::skipTypeInReturn(testMethod.returnType)) {
-                genVoidFunctionAssumes(testMethod, predicateInfo, testedMethod, onlyForOneEntity);
+            if (srcLanguage == utbot::Language::C) {
+                writeTestedFunction(tests, testMethod, predicateInfo, testedMethod, onlyForOneEntity, true);
+                writePosixWrapper(tests, testMethod);
             } else {
-                genNonVoidFunctionAssumes(testMethod, predicateInfo, testedMethod,
-                                          onlyForOneEntity);
+                writeTestedFunction(tests, testMethod, predicateInfo, testedMethod, onlyForOneEntity, false);
             }
-            genGlobalsKleeAssumes(testMethod);
-            genPostParamsKleeAssumes(testMethod);
-            strReturn("0");
-            closeBrackets(1);
         } catch (const UnImplementedException &e) {
             std::string message =
                 "Could not generate klee code for method \'" + methodName + "\', skipping it. ";
@@ -121,11 +150,13 @@ fs::path KleePrinter::writeTmpKleeFile(
 }
 
 void KleePrinter::declTestEntryPoint(const Tests &tests,
-                                     const Tests::MethodDescription &testMethod) {
-    std::string entryPoint = KleeUtils::entryPointFunction(tests, testMethod.name);
+                                     const Tests::MethodDescription &testMethod,
+                                     bool isWrapped) {
+    std::string entryPoint = KleeUtils::entryPointFunction(tests, testMethod.name, false, isWrapped);
     auto argvType = types::Type::createSimpleTypeFromName("char", 2);
     // if change args in next line also change cpp mangledPath in kleeUtils.cpp
-    strFunctionDecl("int", entryPoint, {types::Type::intType(), argvType, argvType}, {"utbot_argc", "utbot_argv", "utbot_envp"}, "") << LB();
+    strFunctionDecl("int", entryPoint, {types::Type::intType(), argvType, argvType},
+                    {PrinterUtils::UTBOT_ARGC, PrinterUtils::UTBOT_ARGV, PrinterUtils::UTBOT_ENVP}, "") << LB();
 }
 
 Tests::MethodParam KleePrinter::getKleeMethodParam(tests::Tests::MethodParam const &param) {
diff --git a/server/src/printers/KleePrinter.h b/server/src/printers/KleePrinter.h
index f2c35c5e..a9d03a71 100644
--- a/server/src/printers/KleePrinter.h
+++ b/server/src/printers/KleePrinter.h
@@ -55,7 +55,7 @@ namespace printer {
             types::Type curType;
         };
 
-        void declTestEntryPoint(const Tests &tests, const Tests::MethodDescription &testMethod);
+        void declTestEntryPoint(const Tests &tests, const Tests::MethodDescription &testMethod, bool isWrapped);
 
         void genGlobalParamsDeclarations(const Tests::MethodDescription &testMethod);
 
@@ -129,6 +129,16 @@ namespace printer {
         void genPostSymbolicVariable(const Tests::MethodDescription &testMethod, const Tests::MethodParam &param);
 
         void genPostAssumes(const Tests::MethodParam &param, bool visitGlobal = false);
+
+        void writePosixWrapper(const Tests &tests,
+                               const tests::Tests::MethodDescription &testMethod);
+
+        void writeTestedFunction(const Tests &tests,
+                                 const tests::Tests::MethodDescription &testMethod,
+                                 const std::optional<LineInfo::PredicateInfo> &predicateInfo,
+                                 const std::string &testedMethod,
+                                 bool onlyForOneEntity,
+                                 bool isWrapped);
     };
 }
 
diff --git a/server/src/utils/KleeUtils.cpp b/server/src/utils/KleeUtils.cpp
index 790ea7a6..132872b6 100644
--- a/server/src/utils/KleeUtils.cpp
+++ b/server/src/utils/KleeUtils.cpp
@@ -81,12 +81,16 @@ namespace KleeUtils {
 
     std::string entryPointFunction(const tests::Tests &tests,
                                    const std::string &methodName,
-                                   bool needToMangle) {
+                                   bool needToMangle,
+                                   bool isWrapped) {
         std::string methodNewName = getRenamedOperator(methodName);
+        if (isWrapped) {
+            methodNewName += PrinterUtils::WRAPPED_SUFFIX;
+        }
         std::string mangledPath = Paths::mangle(tests.relativeFileDir / tests.sourceFileNameNoExt);
         mangledPath = StringUtils::stringFormat("klee_entry__%s_%s", mangledPath, methodNewName);
         if (needToMangle && Paths::isCXXFile(tests.sourceFilePath)) {
-            mangledPath = "_Z" + std::to_string(mangledPath.size()) + mangledPath + "iPPcS0_";
+            mangledPath = PrinterUtils::MANGLED_PREFIX + std::to_string(mangledPath.size()) + mangledPath + PrinterUtils::MANGLED_SUFFIX;
         }
         return mangledPath;
     }
diff --git a/server/src/utils/KleeUtils.h b/server/src/utils/KleeUtils.h
index ded6c23f..bddf63f9 100644
--- a/server/src/utils/KleeUtils.h
+++ b/server/src/utils/KleeUtils.h
@@ -15,8 +15,9 @@ namespace KleeUtils {
     std::string getRenamedOperator(std::string_view methodName);
 
     std::string entryPointFunction(const tests::Tests &tests,
-                              const std::string &methodName,
-                              bool needToMangle = false);
+                                   const std::string &methodName,
+                                   bool needToMangle = false,
+                                   bool isWrapped = false);
 
     std::string postSymbolicVariable(const std::string &variableName);
 
diff --git a/server/src/utils/PrinterUtils.h b/server/src/utils/PrinterUtils.h
index bb70565c..86f51e2f 100644
--- a/server/src/utils/PrinterUtils.h
+++ b/server/src/utils/PrinterUtils.h
@@ -77,6 +77,14 @@ namespace PrinterUtils {
     std::string generateNewVar(int cnt);
 
     const std::string LAZYRENAME = "utbotInnerVar";
+    const std::string UTBOT_ARGC = "utbot_argc";
+    const std::string UTBOT_ARGV = "utbot_argv";
+    const std::string UTBOT_ENVP = "utbot_envp";
+    const std::string POSIX_INIT = "klee_init_env";
+    const std::string WRAPPED_SUFFIX = "__wrapped";
+    const std::string POSIX_CHECK_STDIN_READ = "check_stdin_read";
+    const std::string MANGLED_PREFIX = "_Z";
+    const std::string MANGLED_SUFFIX = "iPPcS0_";
 
     extern const std::string TEST_NAMESPACE;
     extern const std::string DEFINES_FOR_C_KEYWORDS;
diff --git a/server/test/framework/Syntax_Tests.cpp b/server/test/framework/Syntax_Tests.cpp
index cacdc4d6..71b220b4 100644
--- a/server/test/framework/Syntax_Tests.cpp
+++ b/server/test/framework/Syntax_Tests.cpp
@@ -51,6 +51,7 @@ namespace {
         fs::path array_sort_c = getTestFilePath("array_sort.c");
         fs::path stubs_c = getTestFilePath("stubs.c");
         fs::path namespace_cpp = getTestFilePath("namespace.cpp");
+        fs::path input_output_c = getTestFilePath("input_output.c");
 
         void SetUp() override {
             clearEnv(CompilationUtils::CompilerName::CLANG);
@@ -2725,4 +2726,290 @@ namespace {
                 })
         );
     }
+
+    TEST_F(Syntax_Test, simple_getc) {
+        auto [testGen, status] = createTestForFunction(input_output_c, 4);
+
+        ASSERT_TRUE(status.ok()) << status.error_message();
+
+        checkTestCasePredicates(
+            testGen.tests.at(input_output_c).methods.begin().value().testCases,
+            std::vector<TestCasePredicate>(
+                {
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 0;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 1;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 2;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 3;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 4;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 5;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 6;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 7;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 8;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 9;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == -1;
+                    }
+                })
+        );
+    }
+
+    TEST_F(Syntax_Test, simple_fgetc) {
+        auto [testGen, status] = createTestForFunction(input_output_c, 30);
+
+        ASSERT_TRUE(status.ok()) << status.error_message();
+
+        checkTestCasePredicates(
+            testGen.tests.at(input_output_c).methods.begin().value().testCases,
+            std::vector<TestCasePredicate>(
+                {
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 1;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 2;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 3;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 4;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 5;
+                    }
+                })
+        );
+    }
+
+    TEST_F(Syntax_Test, simple_fread) {
+        auto [testGen, status] = createTestForFunction(input_output_c, 53);
+
+        ASSERT_TRUE(status.ok()) << status.error_message();
+
+        checkTestCasePredicates(
+            testGen.tests.at(input_output_c).methods.begin().value().testCases,
+            std::vector<TestCasePredicate>(
+                {
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 0;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 1;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == -1;
+                    }
+                })
+        );
+    }
+
+    TEST_F(Syntax_Test, simple_fgets) {
+        auto [testGen, status] = createTestForFunction(input_output_c, 73);
+
+        ASSERT_TRUE(status.ok()) << status.error_message();
+
+        checkTestCasePredicates(
+            testGen.tests.at(input_output_c).methods.begin().value().testCases,
+            std::vector<TestCasePredicate>(
+                {
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 1;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 0;
+                    }
+                })
+        );
+    }
+
+    TEST_F(Syntax_Test, simple_getchar) {
+        auto [testGen, status] = createTestForFunction(input_output_c, 82);
+
+        ASSERT_TRUE(status.ok()) << status.error_message();
+
+        for (const auto &testCase: testGen.tests.at(input_output_c).methods.begin().value().testCases) {
+            ASSERT_TRUE(stoi(testCase.returnValue.view->getEntryValue(nullptr)) != -1);
+        }
+
+        checkTestCasePredicates(
+            testGen.tests.at(input_output_c).methods.begin().value().testCases,
+            std::vector<TestCasePredicate>(
+                {
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 0;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 1;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 2;
+                    }
+                })
+        );
+    }
+
+    TEST_F(Syntax_Test, simple_gets) {
+        auto [testGen, status] = createTestForFunction(input_output_c, 99);
+
+        ASSERT_TRUE(status.ok()) << status.error_message();
+
+        checkTestCasePredicates(
+            testGen.tests.at(input_output_c).methods.begin().value().testCases,
+            std::vector<TestCasePredicate>(
+                {
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 1;
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return stoi(testCase.returnValue.view->getEntryValue(nullptr)) == 0;
+                    }
+                })
+        );
+    }
+
+    TEST_F(Syntax_Test, simple_putc) {
+        auto [testGen, status] = createTestForFunction(input_output_c, 108);
+
+        ASSERT_TRUE(status.ok()) << status.error_message();
+
+        checkTestCasePredicates(
+            testGen.tests.at(input_output_c).methods.begin().value().testCases,
+            std::vector<TestCasePredicate>(
+                {
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return testCase.returnValue.view->getEntryValue(nullptr) == "'0'";
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return testCase.returnValue.view->getEntryValue(nullptr) == "'1'";
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return testCase.returnValue.view->getEntryValue(nullptr) == "'2'";
+                    }
+                })
+        );
+    }
+
+    TEST_F(Syntax_Test, simple_fputc) {
+        auto [testGen, status] = createTestForFunction(input_output_c, 121);
+
+        ASSERT_TRUE(status.ok()) << status.error_message();
+
+        checkTestCasePredicates(
+            testGen.tests.at(input_output_c).methods.begin().value().testCases,
+            std::vector<TestCasePredicate>(
+                {
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return testCase.returnValue.view->getEntryValue(nullptr) == "'<'";
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return testCase.returnValue.view->getEntryValue(nullptr) == "'>'";
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return testCase.returnValue.view->getEntryValue(nullptr) == "'='";
+                    }
+                })
+        );
+    }
+
+    TEST_F(Syntax_Test, simple_fwrite) {
+        auto [testGen, status] = createTestForFunction(input_output_c, 134);
+
+        ASSERT_TRUE(status.ok()) << status.error_message();
+
+        checkTestCasePredicates(
+            testGen.tests.at(input_output_c).methods.begin().value().testCases,
+            std::vector<TestCasePredicate>(
+                {
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return testCase.returnValue.view->getEntryValue(nullptr) == "'P'";
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return testCase.returnValue.view->getEntryValue(nullptr) == "'N'";
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return testCase.returnValue.view->getEntryValue(nullptr) == "'Z'";
+                    }
+                })
+        );
+    }
+
+    TEST_F(Syntax_Test, simple_fputs) {
+        auto [testGen, status] = createTestForFunction(input_output_c, 150);
+
+        ASSERT_TRUE(status.ok()) << status.error_message();
+
+        checkTestCasePredicates(
+            testGen.tests.at(input_output_c).methods.begin().value().testCases,
+            std::vector<TestCasePredicate>(
+                {
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return testCase.returnValue.view->getEntryValue(nullptr) == "'V'";
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return testCase.returnValue.view->getEntryValue(nullptr) == "'C'";
+                    }
+                })
+        );
+    }
+
+    TEST_F(Syntax_Test, simple_putchar) {
+        auto [testGen, status] = createTestForFunction(input_output_c, 162);
+
+        ASSERT_TRUE(status.ok()) << status.error_message();
+
+        checkTestCasePredicates(
+            testGen.tests.at(input_output_c).methods.begin().value().testCases,
+            std::vector<TestCasePredicate>(
+                {
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return testCase.returnValue.view->getEntryValue(nullptr) == "'>'";
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return testCase.returnValue.view->getEntryValue(nullptr) == "'<'";
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return testCase.returnValue.view->getEntryValue(nullptr) == "'='";
+                    }
+                })
+        );
+    }
+
+    TEST_F(Syntax_Test, simple_puts) {
+        auto [testGen, status] = createTestForFunction(input_output_c, 175);
+
+        ASSERT_TRUE(status.ok()) << status.error_message();
+
+        checkTestCasePredicates(
+            testGen.tests.at(input_output_c).methods.begin().value().testCases,
+            std::vector<TestCasePredicate>(
+                {
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return testCase.returnValue.view->getEntryValue(nullptr) == "'V'";
+                    },
+                    [] (const tests::Tests::MethodTestCase& testCase) {
+                        return testCase.returnValue.view->getEntryValue(nullptr) == "'C'";
+                    }
+                })
+        );
+    }
 }
diff --git a/server/test/suites/syntax/CMakeLists.txt b/server/test/suites/syntax/CMakeLists.txt
index dc0eca57..885a3e82 100644
--- a/server/test/suites/syntax/CMakeLists.txt
+++ b/server/test/suites/syntax/CMakeLists.txt
@@ -37,4 +37,5 @@ add_executable(syntax1
         inner_unnamed.c
         array_sort.c
         stubs.c
-        namespace.cpp)
+        namespace.cpp
+        input_output.c)
diff --git a/server/test/suites/syntax/input_output.c b/server/test/suites/syntax/input_output.c
new file mode 100644
index 00000000..5f6138b7
--- /dev/null
+++ b/server/test/suites/syntax/input_output.c
@@ -0,0 +1,185 @@
+#include <stdio.h>
+#include "input_output.h"
+
+int simple_getc() {
+    unsigned char a = getc(stdin);
+    if (a == '0') {
+        return 0;
+    } else if (a == '1') {
+        return 1;
+    } else if (a == '2') {
+        return 2;
+    } else if (a == '3') {
+        return 3;
+    } else if (a == '4') {
+        return 4;
+    } else if (a == '5') {
+        return 5;
+    } else if (a == '6') {
+        return 6;
+    } else if (a == '7') {
+        return 7;
+    } else if (a == '8') {
+        return 8;
+    } else if (a == '9') {
+        return 9;
+    }
+    return -1;
+}
+
+int simple_fgetc(int x) {
+    if (x >= 0 && x <= 9) {
+        unsigned char a = fgetc(stdin);
+        if (a >= 'a' && a <= 'z') {
+            return 1;
+        } else {
+            return 2;
+        }
+    } else {
+        unsigned char a = fgetc(stdin);
+        unsigned char b = fgetc(stdin);
+        if (a >= 'a' && a <= 'z') {
+            if (b >= '0' && b <= '9') {
+                return 3;
+            } else {
+                return 4;
+            }
+        } else {
+            return 5;
+        }
+    }
+}
+
+int simple_fread() {
+    int arrA[4];
+    int arrB[4];
+    fread(arrA, sizeof(int), 4, stdin);
+    fread(arrB, sizeof(int), 4, stdin);
+
+    int sumA = 0, sumB = 0;
+    for (int i = 0; i < 4; i++) {
+        sumA += arrA[i];
+        sumB += arrB[i];
+    }
+    if (sumA == sumB) {
+        return 0;
+    } else if (sumA > sumB) {
+        return 1;
+    } else {
+        return -1;
+    }
+}
+
+int simple_fgets() {
+    char a[8];
+    fgets(a, 6, stdin);
+    if (a[0] == 'u' && a[1] == 't' && a[2] == 'b' && a[3] == 'o' && a[4] == 't') {
+        return 1;
+    }
+    return 0;
+}
+
+int simple_getchar() {
+    unsigned char a = getchar();
+    unsigned char b = getchar();
+
+    if (a + b < 0) {
+        return -1;
+    }
+
+    if (a + b < 100) {
+        return 0;
+    } else if (a + b < 200) {
+        return 1;
+    } else {
+        return 2;
+    }
+}
+
+int simple_gets() {
+    char a[8];
+    gets(a);
+    if (a[0] == 'u' && a[1] == 't' && a[2] == 'b' && a[3] == 'o' && a[4] == 't') {
+        return 1;
+    }
+    return 0;
+}
+
+char simple_putc(int x, int y) {
+    if (x + y > 0) {
+        putc('1', stdout);
+        return '1';
+    } else if (x + y < 0) {
+        putc('2', stdout);
+        return '2';
+    } else {
+        putc('0', stdout);
+        return '0';
+    }
+}
+
+char simple_fputc(int x, int y) {
+    if (x < y) {
+        fputc('<', stdout);
+        return '<';
+    } else if (x > y) {
+        fputc('>', stdout);
+        return '>';
+    } else {
+        fputc('=', stdout);
+        return '=';
+    }
+}
+
+char simple_fwrite(int x) {
+    if (x > 0) {
+        char a[] = "Positive";
+        fwrite(a, sizeof(char), 8, stdout);
+        return 'P';
+    } else if (x < 0) {
+        char a[] = "Negative";
+        fwrite(a, sizeof(char), 8, stdout);
+        return 'N';
+    } else {
+        char a[] = "Zero";
+        fwrite(a, sizeof(char), 4, stdout);
+        return 'Z';
+    }
+}
+
+char simple_fputs(char c) {
+    if (c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u') {
+        char a[] = "Vowel";
+        fputs("Vowel", stdout);
+        return 'V';
+    } else {
+        char a[] = "Consonant";
+        fputs("Consonant", stdout);
+        return 'C';
+    }
+}
+
+char simple_putchar(int x, int y) {
+    if (3 * x > 2 * y) {
+        putchar('>');
+        return '>';
+    } else if (3 * x < 2 * y) {
+        putchar('<');
+        return '<';
+    } else {
+        putchar('=');
+        return '=';
+    }
+}
+
+char simple_puts(char c) {
+    if (c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u') {
+        char a[] = "Vowel";
+        puts(a);
+        return 'V';
+    } else {
+        char a[] = "Consonant";
+        puts(a);
+        return 'C';
+    }
+}
diff --git a/server/test/suites/syntax/input_output.h b/server/test/suites/syntax/input_output.h
new file mode 100644
index 00000000..9a3e1585
--- /dev/null
+++ b/server/test/suites/syntax/input_output.h
@@ -0,0 +1,28 @@
+#ifndef INPUT_OUTPUT_H
+#define INPUT_OUTPUT_H
+
+int simple_getc();
+
+int simple_fgetc(int x);
+
+int simple_fread();
+
+int simple_fgets();
+
+int simple_getchar();
+
+int simple_gets();
+
+char simple_putc(int x, int y);
+
+char simple_fputc(int x, int y);
+
+char simple_fwrite(int x);
+
+char simple_fputs(char c);
+
+char simple_putchar(int x, int y);
+
+char simple_puts(char c);
+
+#endif
diff --git a/submodules/klee b/submodules/klee
index 73701e2d..0f91b686 160000
--- a/submodules/klee
+++ b/submodules/klee
@@ -1 +1 @@
-Subproject commit 73701e2df1f2ba7a5f34a3f678887cc9d2e444f5
+Subproject commit 0f91b68691d079eb437bb5a381aa91dd40fe5d71