diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 32844fd27c7..b7b9c5b43d9 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -171,6 +171,7 @@ SRC = $(BOOLEFORCE_SRC) \ refinement/string_constraint_generator_testing.cpp \ refinement/string_constraint_generator_transformation.cpp \ refinement/string_constraint_generator_valueof.cpp \ + refinement/string_constraint_instantiation.cpp \ sat/cnf.cpp \ sat/cnf_clause_list.cpp \ sat/dimacs_cnf.cpp \ diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h index 6edb848b550..867284101e3 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/refinement/string_constraint.h @@ -24,6 +24,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include #include +#include #include /*! \brief Universally quantified string constraint @@ -138,12 +139,20 @@ extern inline string_constraintt &to_string_constraint(exprt &expr) return static_cast(expr); } +/// Used for debug printing. +/// \param [in] ns: namespace for `from_expr` +/// \param [in] identifier: identifier for `from_expr` +/// \param [in] expr: constraint to render +/// \return rendered string inline static std::string from_expr( const namespacet &ns, const irep_idt &identifier, const string_constraintt &expr) { - return from_expr(ns, identifier, expr.premise())+" => "+ + return "forall "+from_expr(ns, identifier, expr.univ_var())+" in ["+ + from_expr(ns, identifier, expr.lower_bound())+", "+ + from_expr(ns, identifier, expr.upper_bound())+"). "+ + from_expr(ns, identifier, expr.premise())+" => "+ from_expr(ns, identifier, expr.body()); } @@ -204,6 +213,26 @@ class string_not_contains_constraintt: public exprt } }; +/// Used for debug printing. +/// \param [in] ns: namespace for `from_expr` +/// \param [in] identifier: identifier for `from_expr` +/// \param [in] expr: constraint to render +/// \return rendered string +inline static std::string from_expr( + const namespacet &ns, + const irep_idt &identifier, + const string_not_contains_constraintt &expr) +{ + return "forall x in ["+ + from_expr(ns, identifier, expr.univ_lower_bound())+", "+ + from_expr(ns, identifier, expr.univ_upper_bound())+"). "+ + from_expr(ns, identifier, expr.premise())+" => ("+ + "exists y in ["+from_expr(ns, identifier, expr.exists_lower_bound())+", "+ + from_expr(ns, identifier, expr.exists_upper_bound())+"). "+ + from_expr(ns, identifier, expr.s0())+"[x+y] != "+ + from_expr(ns, identifier, expr.s1())+"[y])"; +} + inline const string_not_contains_constraintt &to_string_not_contains_constraint(const exprt &expr) { diff --git a/src/solvers/refinement/string_constraint_instantiation.cpp b/src/solvers/refinement/string_constraint_instantiation.cpp new file mode 100644 index 00000000000..ca3a63861a2 --- /dev/null +++ b/src/solvers/refinement/string_constraint_instantiation.cpp @@ -0,0 +1,71 @@ +/*******************************************************************\ + +Module: Defines functions related to string constraints. + +Author: Jesse Sigal, jesse.sigal@diffblue.com + +\*******************************************************************/ + +/// \file +/// Defines related function for string constraints. + +#include + +#include +#include +#include + +/// Instantiates a quantified formula representing `not_contains` by +/// substituting the quantifiers and generating axioms. +/// \related string_refinementt +/// \param [in] axiom: the axiom to instantiate +/// \param [in] index_set0: the index set for `axiom.s0()` +/// \param [in] index_set1: the index set for `axiom.s1()` +/// \param [in] generator: generator to be used to get `axiom`'s witness +/// \return the lemmas produced through instantiation +std::vector instantiate_not_contains( + const string_not_contains_constraintt &axiom, + const std::set &index_set0, + const std::set &index_set1, + const string_constraint_generatort &generator) +{ + std::vector lemmas; + + const string_exprt s0=to_string_expr(axiom.s0()); + const string_exprt s1=to_string_expr(axiom.s1()); + + for(const auto &i0 : index_set0) + for(const auto &i1 : index_set1) + { + const minus_exprt val(i0, i1); + const exprt witness=generator.get_witness_of(axiom, val); + const and_exprt prem_and_is_witness( + axiom.premise(), + equal_exprt(witness, i1)); + + const not_exprt differ(equal_exprt(s0[i0], s1[i1])); + const implies_exprt lemma(prem_and_is_witness, differ); + lemmas.push_back(lemma); + + // we put bounds on the witnesses: + // 0 <= v <= |s0| - |s1| ==> 0 <= v+w[v] < |s0| && 0 <= w[v] < |s1| + const exprt zero=from_integer(0, val.type()); + const binary_relation_exprt c1(zero, ID_le, plus_exprt(val, witness)); + const binary_relation_exprt c2( + s0.length(), ID_gt, plus_exprt(val, witness)); + const binary_relation_exprt c3(s1.length(), ID_gt, witness); + const binary_relation_exprt c4(zero, ID_le, witness); + + const minus_exprt diff(s0.length(), s1.length()); + + const and_exprt premise( + binary_relation_exprt(zero, ID_le, val), + binary_relation_exprt(diff, ID_ge, val)); + const implies_exprt witness_bounds( + premise, + and_exprt(and_exprt(c1, c2), and_exprt(c3, c4))); + lemmas.push_back(witness_bounds); + } + + return lemmas; +} diff --git a/src/solvers/refinement/string_constraint_instantiation.h b/src/solvers/refinement/string_constraint_instantiation.h new file mode 100644 index 00000000000..f4918e7e8d9 --- /dev/null +++ b/src/solvers/refinement/string_constraint_instantiation.h @@ -0,0 +1,24 @@ +/*******************************************************************\ + +Module: Defines related function for string constraints. + +Author: Jesse Sigal, jesse.sigal@diffblue.com + +\*******************************************************************/ + +/// \file +/// Defines related function for string constraints. + +#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H +#define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H + +#include +#include + +std::vector instantiate_not_contains( + const string_not_contains_constraintt &axiom, + const std::set &index_set0, + const std::set &index_set1, + const string_constraint_generatort &generator); + +#endif // CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 95e84d422a4..1c9297b5e65 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -29,6 +29,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #include #include #include +#include #include #include @@ -606,8 +607,8 @@ decision_proceduret::resultt string_refinementt::dec_solve() for(unsigned i=0; i lemmas; - instantiate_not_contains(not_contains_axioms[i], lemmas); + const std::vector lemmas= + instantiate_not_contains(not_contains_axioms[i]); for(const exprt &lemma : lemmas) add_lemma(lemma); } @@ -1603,60 +1604,23 @@ exprt string_refinementt::instantiate( return implies_exprt(bounds, instance); } -/// instantiate a quantified formula representing `not_contains` by substituting -/// the quantifiers and generating axioms -/// \par parameters: a quantified formula representing `not_contains`, and a -/// list to which to add the created lemmas to -void string_refinementt::instantiate_not_contains( - const string_not_contains_constraintt &axiom, std::list &new_lemmas) +/// Instantiates a quantified formula representing `not_contains` by +/// substituting the quantifiers and generating axioms. +/// \param [in] axiom: the axiom to instantiate +/// \return the lemmas produced through instantiation +std::vector string_refinementt::instantiate_not_contains( + const string_not_contains_constraintt &axiom) { - exprt s0=axiom.s0(); - exprt s1=axiom.s1(); + const string_exprt s0=to_string_expr(axiom.s0()); + const string_exprt s1=to_string_expr(axiom.s1()); debug() << "instantiate not contains " << from_expr(ns, "", s0) << " : " << from_expr(ns, "", s1) << eom; - expr_sett index_set0=index_set[to_string_expr(s0).content()]; - expr_sett index_set1=index_set[to_string_expr(s1).content()]; + const expr_sett index_set0=index_set[s0.content()]; + const expr_sett index_set1=index_set[s1.content()]; - for(auto it0 : index_set0) - for(auto it1 : index_set1) - { - debug() << from_expr(ns, "", it0) << " : " << from_expr(ns, "", it1) - << eom; - exprt val=minus_exprt(it0, it1); - exprt witness=generator.get_witness_of(axiom, val); - and_exprt prem_and_is_witness( - axiom.premise(), - equal_exprt(witness, it1)); - - not_exprt differ( - equal_exprt( - to_string_expr(s0)[it0], - to_string_expr(s1)[it1])); - exprt lemma=implies_exprt(prem_and_is_witness, differ); - - new_lemmas.push_back(lemma); - // we put bounds on the witnesses: - // 0 <= v <= |s0| - |s1| ==> 0 <= v+w[v] < |s0| && 0 <= w[v] < |s1| - exprt zero=from_integer(0, val.type()); - binary_relation_exprt c1(zero, ID_le, plus_exprt(val, witness)); - binary_relation_exprt c2 - (to_string_expr(s0).length(), ID_gt, plus_exprt(val, witness)); - binary_relation_exprt c3(to_string_expr(s1).length(), ID_gt, witness); - binary_relation_exprt c4(zero, ID_le, witness); - - minus_exprt diff( - to_string_expr(s0).length(), - to_string_expr(s1).length()); - - and_exprt premise( - binary_relation_exprt(zero, ID_le, val), - binary_relation_exprt(diff, ID_ge, val)); - exprt witness_bounds=implies_exprt( - premise, - and_exprt(and_exprt(c1, c2), and_exprt(c3, c4))); - new_lemmas.push_back(witness_bounds); - } + return ::instantiate_not_contains( + axiom, index_set0, index_set1, generator); } /// replace array-lists by 'with' expressions diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 3a83734b1d5..64e54cb8e15 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -133,9 +133,8 @@ class string_refinementt: public bv_refinementt exprt instantiate( const string_constraintt &axiom, const exprt &str, const exprt &val); - void instantiate_not_contains( - const string_not_contains_constraintt &axiom, - std::list &new_lemmas); + std::vector instantiate_not_contains( + const string_not_contains_constraintt &axiom); exprt substitute_array_lists(exprt) const; diff --git a/unit/Makefile b/unit/Makefile index 63a6acb4fda..75960795d12 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -24,6 +24,7 @@ SRC += unit_tests.cpp \ solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \ solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \ solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix_lower_case.cpp \ + solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \ catch_example.cpp \ # Empty last line diff --git a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp new file mode 100644 index 00000000000..872fe3537d6 --- /dev/null +++ b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp @@ -0,0 +1,491 @@ +/*******************************************************************\ + + Module: Unit tests for `instantiate_not_contains_`. + + Author: Jesse Sigal, jesse.sigal@diffblue.com + +\*******************************************************************/ + +#include + +#include + +#include +#include +#include +#include +#include +#include +#include +#include + +/// \class Types used throughout the test. Currently it is impossible to +/// statically initialize this value, there is a PR to allow this +/// diffblue/cbmc/pull/1213 +class tt +{ +public: + tt() {} + typet char_type() const {return java_char_type();} + typet length_type() const {return java_int_type();} + array_typet array_type() const + { + return array_typet(char_type(), infinity_exprt(length_type())); + } + refined_string_typet string_type() const + { + return refined_string_typet(length_type(), char_type()); + } + array_typet witness_type() const + { + return array_typet(length_type(), infinity_exprt(length_type())); + } +}; + +// Static variable to get proper types +const tt t; + +/// Creates a `constant_exprt` of the proper length type. +/// \param [in] i: integer to convert +/// \return corresponding `constant_exprt` +constant_exprt from_integer(const mp_integer i) +{ + return from_integer(i, t.length_type()); +} + +/// Creates a `string_exprt` of the proper string type. +/// \param [in] str: string to convert +/// \return corresponding `string_exprt` +string_exprt make_string_exprt(const std::string &str) +{ + const constant_exprt length=from_integer(str.length(), t.length_type()); + array_exprt content(t.array_type()); + + for(const char c : str) + content.copy_to_operands(from_integer(c, t.char_type())); + + return string_exprt(length, content, t.string_type()); +} + +/// For a constant `string_exprt`, creates a full index set. +/// \param [in] s: `string_exprt` to create index set for +/// \return the corresponding index set +std::set full_index_set(const string_exprt &s) +{ + PRECONDITION(s.length().is_constant()); + mp_integer n; + to_integer(s.length(), n); + std::set ret; + for(mp_integer i=0; i &lemmas, const namespacet &ns) +{ + // Conjunction of new lemmas + exprt conj=conjunction(lemmas); + + // Simplify + simplify(conj, ns); + + return conj; +} + +/// Creates information string and simplifies lemmas. +/// \param [in,out] lemmas: lemmas to process (which are simplified) +/// \param [in] ns: namespace for printing and simplifying +/// \return information string +std::string create_info(std::vector &lemmas, const namespacet &ns) +{ + // Recording new lemmas + std::string new_lemmas; + for(auto &lemma : lemmas) + { + simplify(lemma, ns); + new_lemmas+=from_expr(ns, "", lemma)+"\n\n"; + } + return "Instantiated lemmas:\n"+new_lemmas; +} + +/// Checks the satisfiability of the given expression. +/// \param [in] expr: expression to check +/// \param [in] ns: namespace for solver +/// \return SAT solver result +decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns) +{ + satcheck_no_simplifiert sat_check; + bv_refinementt solver(ns, sat_check); + solver << expr; + return solver(); +} + +// The [!mayfail] tag allows tests to fail while reporting the failure +SCENARIO("instantiate_not_contains", + "[!mayfail][core][solvers][refinement][string_constraint_instantiation]") +{ + // For printing expression + register_language(new_java_bytecode_language); + symbol_tablet symtbl; + const namespacet ns(symtbl); + + GIVEN("The not_contains axioms of String.lastIndexOf(String, Int)") + { + // Creating strings + const string_exprt ab=make_string_exprt("ab"); + const string_exprt b=make_string_exprt("b"); + + // Creating "ab".lastIndexOf("b", 0) + function_application_exprt func( + symbol_exprt(ID_cprover_string_last_index_of_func), t.length_type()); + const exprt::operandst args={ab, b, from_integer(2)}; + func.arguments()=args; + + // Generating the corresponding axioms and simplifying, recording info + string_constraint_generatort generator; + exprt res=generator.add_axioms_for_function_application(func); + std::string axioms; + std::vector nc_axioms; + for(auto &axiom : generator.axioms) + { + simplify(axiom, ns); + if(axiom.id()==ID_string_constraint) + { + string_constraintt sc=to_string_constraint(axiom); + axioms+=from_expr(ns, "", sc); + } + else if(axiom.id()==ID_string_not_contains_constraint) + { + string_not_contains_constraintt sc= + to_string_not_contains_constraint(axiom); + axioms+=from_expr(ns, "", sc); + generator.witness[sc]= + generator.fresh_symbol("w", t.witness_type()); + nc_axioms.push_back(sc); + } + else + axioms+=from_expr(ns, "", axiom); + + axioms+="\n\n"; + } + INFO("Original axioms:\n"); + INFO(axioms); + + WHEN("we instantiate and simplify") + { + // Making index sets + const std::set index_set_ab=full_index_set(ab); + const std::set index_set_b=full_index_set(b); + + // List of new lemmas to be returned + std::vector lemmas; + + // Instantiate the lemmas + for(const auto &axiom : nc_axioms) + { + const std::vector l=instantiate_not_contains( + axiom, index_set_ab, index_set_b, generator); + lemmas.insert(lemmas.end(), l.begin(), l.end()); + } + + const exprt conj=combine_lemmas(lemmas, ns); + const std::string info=create_info(lemmas, ns); + INFO(info); + + THEN("the conjunction of instantiations is SAT") + { + // Check if SAT + decision_proceduret::resultt result=check_sat(conj, ns); + + // Require SAT + if(result==decision_proceduret::resultt::D_ERROR) + INFO("Got an error"); + + REQUIRE(result==decision_proceduret::resultt::D_SATISFIABLE); + } + } + } + + GIVEN("A vacuously true not_contains axioms") + { + // Creating strings + const string_exprt a=make_string_exprt("a"); + + // Make + // forall x in [0, 0). true => (exists y in [0, 1). + // { .=1, .={ (char)'a' } }[x+y] != { .=1, .={ (char)'b' } }[y] + // ) + // which is vacuously true. + string_not_contains_constraintt vacuous( + from_integer(0), + from_integer(0), + true_exprt(), + from_integer(0), + from_integer(1), + a, + a); + + // Create witness for axiom + string_constraint_generatort generator; + generator.witness[vacuous]= + generator.fresh_symbol("w", t.witness_type()); + + INFO("Original axiom:\n"); + INFO(from_expr(ns, "", vacuous)+"\n\n"); + + WHEN("we instantiate and simplify") + { + // Making index sets + const std::set index_set_a=full_index_set(a); + + // Instantiate the lemmas + std::vector lemmas=instantiate_not_contains( + vacuous, index_set_a, index_set_a, generator); + + const exprt conj=combine_lemmas(lemmas, ns); + const std::string info=create_info(lemmas, ns); + INFO(info); + + THEN("the conjunction of instantiations is SAT") + { + // Check if SAT + decision_proceduret::resultt result=check_sat(conj, ns); + + // Require SAT + if(result==decision_proceduret::resultt::D_ERROR) + INFO("Got an error"); + + REQUIRE(result==decision_proceduret::resultt::D_SATISFIABLE); + } + } + } + + GIVEN("A trivially false (via empty existential) not_contains axioms") + { + // Creating strings + const string_exprt a=make_string_exprt("a"); + const string_exprt b=make_string_exprt("b"); + + // Make + // forall x in [0, 1). true => (exists y in [0, 0). + // { .=1, .={ (char)'a' } }[x+y] != { .=1, .={ (char)'b' } }[y] + // ) + // which is false. + string_not_contains_constraintt trivial( + from_integer(0), + from_integer(1), + true_exprt(), + from_integer(0), + from_integer(0), + a, + b); + + // Create witness for axiom + string_constraint_generatort generator; + generator.witness[trivial]= + generator.fresh_symbol("w", t.witness_type()); + + INFO("Original axiom:\n"); + INFO(from_expr(ns, "", trivial)+"\n\n"); + + WHEN("we instantiate and simplify") + { + // Making index sets + const std::set index_set_a=full_index_set(a); + const std::set index_set_b=full_index_set(b); + + // Instantiate the lemmas + std::vector lemmas=instantiate_not_contains( + trivial, index_set_a, index_set_b, generator); + + const exprt conj=combine_lemmas(lemmas, ns); + const std::string info=create_info(lemmas, ns); + INFO(info); + + THEN("the conjunction of instantiations is UNSAT") + { + // Check if SAT + decision_proceduret::resultt result=check_sat(conj, ns); + + // Require UNSAT + if(result==decision_proceduret::resultt::D_ERROR) + INFO("Got an error"); + + REQUIRE(result==decision_proceduret::resultt::D_UNSATISFIABLE); + } + } + } + + GIVEN("A not_contains axioms with an non-empty and empty string") + { + // Creating strings + const string_exprt a=make_string_exprt("a"); + const string_exprt empty=make_string_exprt(""); + + // Make + // forall x in [0, 1). true => (exists y in [0, 0). + // { .=1, .={ (char)'a' } }[x+y] != { .=0, .={ } }[y] + // ) + // which is false. + string_not_contains_constraintt trivial( + from_integer(0), + from_integer(1), + true_exprt(), + from_integer(0), + from_integer(0), + a, + empty); + + // Create witness for axiom + string_constraint_generatort generator; + generator.witness[trivial]= + generator.fresh_symbol("w", t.witness_type()); + + INFO("Original axiom:\n"); + INFO(from_expr(ns, "", trivial)+"\n\n"); + + WHEN("we instantiate and simplify") + { + // Making index sets + const std::set index_set_a=full_index_set(a); + const std::set index_set_empty= + {generator.fresh_exist_index("z", t.length_type())}; + + // Instantiate the lemmas + std::vector lemmas=instantiate_not_contains( + trivial, index_set_a, index_set_empty, generator); + + const exprt conj=combine_lemmas(lemmas, ns); + const std::string info=create_info(lemmas, ns); + INFO(info); + + THEN("the conjunction of instantiations is UNSAT") + { + // Check if SAT + decision_proceduret::resultt result=check_sat(conj, ns); + + // Require UNSAT + if(result==decision_proceduret::resultt::D_ERROR) + INFO("Got an error"); + + REQUIRE(result==decision_proceduret::resultt::D_UNSATISFIABLE); + } + } + } + + GIVEN("A not_contains on the same string twice (hence is false)") + { + // Creating strings + const string_exprt ab=make_string_exprt("ab"); + + // Make + // forall x in [0, 2). true => (exists y in [0, 2). + // { .=2, .={ (char)'a', (char)'b'} }[x+y] != + // { .=2, .={ (char)'a', (char)'b'}[y] + // ) + // which is false (for x = 0). + string_not_contains_constraintt trivial( + from_integer(0), + from_integer(2), + true_exprt(), + from_integer(0), + from_integer(2), + ab, + ab); + + // Create witness for axiom + string_constraint_generatort generator; + generator.witness[trivial]= + generator.fresh_symbol("w", t.witness_type()); + + INFO("Original axiom:\n"); + INFO(from_expr(ns, "", trivial)+"\n\n"); + + WHEN("we instantiate and simplify") + { + // Making index sets + const std::set index_set_ab=full_index_set(ab); + + // Instantiate the lemmas + std::vector lemmas=instantiate_not_contains( + trivial, index_set_ab, index_set_ab, generator); + + const exprt conj=combine_lemmas(lemmas, ns); + const std::string info=create_info(lemmas, ns); + INFO(info); + + THEN("the conjunction of instantiations is UNSAT") + { + // Check if SAT + decision_proceduret::resultt result=check_sat(conj, ns); + + // Require UNSAT + if(result==decision_proceduret::resultt::D_ERROR) + INFO("Got an error"); + + REQUIRE(result==decision_proceduret::resultt::D_UNSATISFIABLE); + } + } + } + + GIVEN("A not_contains on two string with no chars in common (hence is true)") + { + // Creating strings + const string_exprt ab=make_string_exprt("ab"); + const string_exprt cd=make_string_exprt("cd"); + + // Make + // forall x in [0, 2). true => (exists y in [0, 2). + // { .=2, .={ (char)'a', (char)'b'} }[x+y] != + // { .=2, .={ (char)'a', (char)'b'}[y] + // ) + // which is true. + string_not_contains_constraintt trivial( + from_integer(0), + from_integer(2), + true_exprt(), + from_integer(0), + from_integer(2), + ab, + cd); + + // Create witness for axiom + string_constraint_generatort generator; + generator.witness[trivial]= + generator.fresh_symbol("w", t.witness_type()); + + INFO("Original axiom:\n"); + INFO(from_expr(ns, "", trivial)+"\n\n"); + + WHEN("we instantiate and simplify") + { + // Making index sets + const std::set index_set_ab=full_index_set(ab); + const std::set index_set_cd=full_index_set(cd); + + // Instantiate the lemmas + std::vector lemmas=instantiate_not_contains( + trivial, index_set_ab, index_set_cd, generator); + + const exprt conj=combine_lemmas(lemmas, ns); + const std::string info=create_info(lemmas, ns); + INFO(info); + + THEN("the conjunction of instantiations is SAT") + { + // Check if SAT + decision_proceduret::resultt result=check_sat(conj, ns); + + // Require UNSAT + if(result==decision_proceduret::resultt::D_ERROR) + INFO("Got an error"); + + REQUIRE(result==decision_proceduret::resultt::D_SATISFIABLE); + } + } + } +}