| 1884 | } |
| 1885 | |
| 1886 | CHCSolverInterface::QueryResult CHC::query(smtutil::Expression const& _query, langutil::SourceLocation const& _location) |
| 1887 | { |
| 1888 | if (m_settings.printQuery) |
| 1889 | { |
| 1890 | auto smtLibInterface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get()); |
| 1891 | solAssert(smtLibInterface, "Requested to print queries but CHCSmtLib2Interface not available"); |
| 1892 | std::string smtLibCode = smtLibInterface->dumpQuery(_query); |
| 1893 | m_errorReporter.info( |
| 1894 | 2339_error, |
| 1895 | "CHC: Requested query:\n" + smtLibCode |
| 1896 | ); |
| 1897 | return {.answer = CheckResult::UNKNOWN, .invariants = {}, .cex = {}}; |
| 1898 | } |
| 1899 | auto result = m_interface->query(_query); |
| 1900 | switch (result.answer) |
| 1901 | { |
| 1902 | case CheckResult::SATISFIABLE: |
| 1903 | case CheckResult::UNSATISFIABLE: |
| 1904 | case CheckResult::UNKNOWN: |
| 1905 | break; |
| 1906 | case CheckResult::CONFLICTING: |
| 1907 | m_errorReporter.warning(1988_error, _location, "CHC: At least two SMT solvers provided conflicting answers. Results might not be sound."); |
| 1908 | break; |
| 1909 | case CheckResult::ERROR: |
| 1910 | m_errorReporter.warning(1218_error, _location, "CHC: Error during interaction with the solver."); |
| 1911 | break; |
| 1912 | } |
| 1913 | return result; |
| 1914 | } |
| 1915 | |
| 1916 | void CHC::verificationTargetEncountered( |
| 1917 | ASTNode const* const _errorNode, |