From 2cf12a56cb9c5eb539d50a39b2764a292d6fd13f Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Tue, 13 Nov 2012 04:49:34 +0000 Subject: [PATCH] added support for division by zero for bit-vector division operators --- src/smt/smt_engine.cpp | 95 ++++++++++++++++++- src/theory/bv/bitblast_strategies.cpp | 8 +- src/theory/bv/bitblaster.cpp | 22 ++++- src/theory/bv/bv_subtheory_eq.cpp | 16 +++- src/theory/bv/bv_subtheory_eq.h | 2 + src/theory/bv/kinds | 6 ++ ...ory_bv_rewrite_rules_constant_evaluation.h | 4 +- .../theory_bv_rewrite_rules_simplification.h | 12 +-- src/theory/bv/theory_bv_rewriter.cpp | 11 ++- src/theory/bv/theory_bv_rewriter.h | 4 +- .../regress0/unconstrained/Makefile.am | 4 +- .../regress0/unconstrained/bvdiv2.smt2 | 8 +- 12 files changed, 158 insertions(+), 34 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6079f146e..1fc32917e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -41,6 +41,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/theory_engine.h" +#include "theory/bv/theory_bv_rewrite_rules.h" #include "proof/proof_manager.h" #include "util/proof.h" #include "util/boolean_simplification.h" @@ -226,6 +227,14 @@ class SmtEnginePrivate : public NodeManagerListener { */ Node d_divByZero; + /** + * Maps from bit-vector width to divison-by-zero uninterpreted + * function symbols. + */ + hash_map d_BVDivByZero; + hash_map d_BVRemByZero; + + /** * Function symbol used to implement uninterpreted * int-division-by-zero semantics. Needed to deal with partial @@ -400,6 +409,23 @@ public: void addFormula(TNode n) throw(TypeCheckingException, LogicException); + /** + * Return the uinterpreted function symbol corresponding to division-by-zero + * for this particular bit-wdith + * @param k should be UREM or UDIV + * @param width + * + * @return + */ + Node getBVDivByZero(Kind k, unsigned width); + /** + * Returns the node modeling the division-by-zero semantics of node n. + * + * @param n + * + * @return + */ + Node expandBVDivByZero(TNode n); /** * Expand definitions in n. */ @@ -691,8 +717,8 @@ void SmtEngine::setLogicInternal() throw() { d_logic.lock(); // may need to force uninterpreted functions to be on for non-linear - if(d_logic.isTheoryEnabled(theory::THEORY_ARITH) && - !d_logic.isLinear() && + if(((d_logic.isTheoryEnabled(theory::THEORY_ARITH) && !d_logic.isLinear()) || + d_logic.isTheoryEnabled(theory::THEORY_BV)) && !d_logic.isTheoryEnabled(theory::THEORY_UF)){ d_logic = d_logic.getUnlockedCopy(); d_logic.enableTheory(theory::THEORY_UF); @@ -1101,6 +1127,53 @@ void SmtEngine::defineFunction(Expr func, d_definedFunctions->insert(funcNode, def); } + +Node SmtEnginePrivate::getBVDivByZero(Kind k, unsigned width) { + NodeManager* nm = d_smt.d_nodeManager; + if (k == kind::BITVECTOR_UDIV) { + if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) { + // lazily create the function symbols + std::ostringstream os; + os << "BVUDivByZero_" << width; + Node divByZero = nm->mkSkolem(os.str(), + nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)), + "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME); + d_BVDivByZero[width] = divByZero; + } + return d_BVDivByZero[width]; + } + else if (k == kind::BITVECTOR_UREM) { + if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) { + std::ostringstream os; + os << "BVURemByZero_" << width; + Node divByZero = nm->mkSkolem(os.str(), + nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)), + "partial bvurem", NodeManager::SKOLEM_EXACT_NAME); + d_BVRemByZero[width] = divByZero; + } + return d_BVRemByZero[width]; + } + + Unreachable(); +} + + +Node SmtEnginePrivate::expandBVDivByZero(TNode n) { + // we only deal wioth the unsigned division operators as the signed ones should have been + // expanded in terms of the unsigned operators + NodeManager* nm = d_smt.d_nodeManager; + unsigned width = n.getType().getBitVectorSize(); + Node divByZero = getBVDivByZero(n.getKind(), width); + TNode num = n[0], den = n[1]; + Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(BitVector(width, Integer(0)))); + Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num); + Node divTotalNumDen = nm->mkNode(n.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : + kind::BITVECTOR_UREM_TOTAL, num, den); + Node node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); + return node; +} + + Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map& cache) throw(TypeCheckingException, LogicException) { @@ -1120,10 +1193,26 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map, + bv::RewriteRule, + bv::RewriteRule + >::apply(node); + break; + } + + case kind::BITVECTOR_UDIV: + case kind::BITVECTOR_UREM: { + node = expandBVDivByZero(node); + break; + } case kind::DIVISION: { // partial function: division if(d_smt.d_logic.isLinear()) { diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index d2fbb432b..fbf9a45ee 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -640,7 +640,7 @@ void uDivModRec(const Bits& a, const Bits& b, Bits& q, Bits& r, unsigned rec_wid void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) { BVDebug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_UDIV && q.size() == 0); + Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL && q.size() == 0); Bits a, b; bb->bbTerm(node[0], a); @@ -650,13 +650,13 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) { uDivModRec(a, b, q, r, getSize(node)); // cache the remainder in case we need it later - Node remainder = mkNode(kind::BITVECTOR_UREM, node[0], node[1]); + Node remainder = mkNode(kind::BITVECTOR_UREM_TOTAL, node[0], node[1]); bb->cacheTermDef(remainder, r); } void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) { BVDebug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_UREM && rem.size() == 0); + Assert(node.getKind() == kind::BITVECTOR_UREM_TOTAL && rem.size() == 0); Bits a, b; bb->bbTerm(node[0], a); @@ -666,7 +666,7 @@ void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) { uDivModRec(a, b, q, rem, getSize(node)); // cache the quotient in case we need it later - Node quotient = mkNode(kind::BITVECTOR_UDIV, node[0], node[1]); + Node quotient = mkNode(kind::BITVECTOR_UDIV_TOTAL, node[0], node[1]); bb->cacheTermDef(quotient, q); } diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 41d98326e..aca81e176 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -214,6 +214,13 @@ bool Bitblaster::assertToSat(TNode lit, bool propagate) { */ bool Bitblaster::solve(bool quick_solve) { + if (Trace.isOn("bitvector")) { + Trace("bitvector") << "Bitblaster::solve() asserted atoms "; + context::CDList::const_iterator it = d_assertedAtoms.begin(); + for (; it != d_assertedAtoms.end(); ++it) { + Trace("bitvector") << " " << d_cnfStream->getNode(*it) << "\n"; + } + } BVDebug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; return SAT_VALUE_TRUE == d_satSolver->solve(); } @@ -280,11 +287,13 @@ void Bitblaster::initTermBBStrategies() { d_termBBStrategies [ kind::BITVECTOR_PLUS ] = DefaultPlusBB; d_termBBStrategies [ kind::BITVECTOR_SUB ] = DefaultSubBB; d_termBBStrategies [ kind::BITVECTOR_NEG ] = DefaultNegBB; - d_termBBStrategies [ kind::BITVECTOR_UDIV ] = DefaultUdivBB; - d_termBBStrategies [ kind::BITVECTOR_UREM ] = DefaultUremBB; - d_termBBStrategies [ kind::BITVECTOR_SDIV ] = DefaultSdivBB; - d_termBBStrategies [ kind::BITVECTOR_SREM ] = DefaultSremBB; - d_termBBStrategies [ kind::BITVECTOR_SMOD ] = DefaultSmodBB; + d_termBBStrategies [ kind::BITVECTOR_UDIV ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_UREM ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_UDIV_TOTAL ] = DefaultUdivBB; + d_termBBStrategies [ kind::BITVECTOR_UREM_TOTAL ] = DefaultUremBB; + d_termBBStrategies [ kind::BITVECTOR_SDIV ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_SREM ] = UndefinedTermBBStrategy; + d_termBBStrategies [ kind::BITVECTOR_SMOD ] = UndefinedTermBBStrategy; d_termBBStrategies [ kind::BITVECTOR_SHL ] = DefaultShlBB; d_termBBStrategies [ kind::BITVECTOR_LSHR ] = DefaultLshrBB; d_termBBStrategies [ kind::BITVECTOR_ASHR ] = DefaultAshrBB; @@ -429,6 +438,9 @@ void Bitblaster::collectModelInfo(TheoryModel* m) { TNode var = *it; if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { Node const_value = getVarValue(var); + Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= " + << var << " " + << const_value << "))\n"; m->assertEquality(var, const_value, true); } } diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp index 17f3acdd1..e809a2566 100644 --- a/src/theory/bv/bv_subtheory_eq.cpp +++ b/src/theory/bv/bv_subtheory_eq.cpp @@ -28,7 +28,8 @@ using namespace CVC4::theory::bv::utils; EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv) : SubtheorySolver(c, bv), d_notify(*this), - d_equalityEngine(d_notify, c, "theory::bv::TheoryBV") + d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"), + d_assertions(c) { if (d_useEqualityEngine) { @@ -87,14 +88,16 @@ void EqualitySolver::explain(TNode literal, std::vector& assumptions) { } bool EqualitySolver::addAssertions(const std::vector& assertions, Theory::Effort e) { - BVDebug("bitvector::equality") << "EqualitySolver::addAssertions \n"; + Trace("bitvector::equality") << "EqualitySolver::addAssertions \n"; Assert (!d_bv->inConflict()); for (unsigned i = 0; i < assertions.size(); ++i) { TNode fact = assertions[i]; - + // Notify the equality engine if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_EQUALITY) ) { + Trace("bitvector::equality") << " (assert " << fact << ")\n"; + d_assertions.push_back(fact); bool negated = fact.getKind() == kind::NOT; TNode predicate = negated ? fact[0] : fact; if (predicate.getKind() == kind::EQUAL) { @@ -164,5 +167,12 @@ void EqualitySolver::conflict(TNode a, TNode b) { } void EqualitySolver::collectModelInfo(TheoryModel* m) { + if (Debug.isOn("bitvector-model")) { + context::CDList::const_iterator it = d_assertions.begin(); + for (; it!= d_assertions.end(); ++it) { + Debug("bitvector-model") << "EqualitySolver::collectModelInfo (assert " + << *it << ")\n"; + } + } m->assertEqualityEngine(&d_equalityEngine); } diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_eq.h index 91ad1599b..64fe12706 100644 --- a/src/theory/bv/bv_subtheory_eq.h +++ b/src/theory/bv/bv_subtheory_eq.h @@ -58,6 +58,8 @@ class EqualitySolver : public SubtheorySolver { /** Store a conflict from merging two constants */ void conflict(TNode a, TNode b); + /** FIXME: for debugging purposes only */ + context::CDList d_assertions; public: EqualitySolver(context::Context* c, TheoryBV* bv); diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 9dc2e66bb..2faa12437 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -54,6 +54,10 @@ operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating divisio operator BITVECTOR_SDIV 2 "bit-vector 2's complement signed division" operator BITVECTOR_SREM 2 "bit-vector 2's complement signed remainder (sign follows dividend)" operator BITVECTOR_SMOD 2 "bit-vector 2's complement signed remainder (sign follows divisor)" +# total division kinds +operator BITVECTOR_UDIV_TOTAL 2 "bit-vector total unsigned division, truncating towards 0 (undefined if divisor is 0)" +operator BITVECTOR_UREM_TOTAL 2 "bit-vector total unsigned remainder from truncating division (undefined if divisor is 0)" + operator BITVECTOR_SHL 2 "bit-vector left shift" operator BITVECTOR_LSHR 2 "bit-vector logical shift right" operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right" @@ -135,6 +139,8 @@ typerule BITVECTOR_NEG ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_UDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_UREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_UDIV_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_UREM_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_SMOD ::CVC4::theory::bv::BitVectorFixedWidthTypeRule diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index d7d7c9670..8b080d104 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -198,7 +198,7 @@ Node RewriteRule::apply(TNode node) { } template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UDIV && + return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL && utils::isBVGroundTerm(node)); } @@ -213,7 +213,7 @@ Node RewriteRule::apply(TNode node) { } template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UREM && + return (node.getKind() == kind::BITVECTOR_UREM_TOTAL && utils::isBVGroundTerm(node)); } diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index a2fd9ee19..23cd8381d 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -752,7 +752,7 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UDIV && + return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL && utils::isPow2Const(node[1])); } @@ -776,7 +776,7 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UDIV && + return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL && node[1] == utils::mkConst(utils::getSize(node), 1)); } @@ -794,7 +794,7 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UDIV && + return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL && node[0] == node[1]); } @@ -812,7 +812,7 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UREM && + return (node.getKind() == kind::BITVECTOR_UREM_TOTAL && utils::isPow2Const(node[1])); } @@ -837,7 +837,7 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UREM && + return (node.getKind() == kind::BITVECTOR_UREM_TOTAL && node[1] == utils::mkConst(utils::getSize(node), 1)); } @@ -855,7 +855,7 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_UREM && + return (node.getKind() == kind::BITVECTOR_UREM_TOTAL && node[0] == node[1]); } diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index a8941aac2..1335f8f4a 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -365,7 +365,8 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool preregister) { return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool preregister){ + +RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool preregister){ Node resultNode = node; if(RewriteRule::applies(node)) { @@ -382,7 +383,7 @@ RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool preregister){ return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool preregister) { Node resultNode = node; if(RewriteRule::applies(node)) { @@ -575,8 +576,10 @@ void TheoryBVRewriter::initializeRewrites() { d_rewriteTable [ kind::BITVECTOR_PLUS ] = RewritePlus; d_rewriteTable [ kind::BITVECTOR_SUB ] = RewriteSub; d_rewriteTable [ kind::BITVECTOR_NEG ] = RewriteNeg; - d_rewriteTable [ kind::BITVECTOR_UDIV ] = RewriteUdiv; - d_rewriteTable [ kind::BITVECTOR_UREM ] = RewriteUrem; + // d_rewriteTable [ kind::BITVECTOR_UDIV ] = RewriteUdiv; + // d_rewriteTable [ kind::BITVECTOR_UREM ] = RewriteUrem; + d_rewriteTable [ kind::BITVECTOR_UDIV_TOTAL ] = RewriteUdivTotal; + d_rewriteTable [ kind::BITVECTOR_UREM_TOTAL ] = RewriteUremTotal; d_rewriteTable [ kind::BITVECTOR_SMOD ] = RewriteSmod; d_rewriteTable [ kind::BITVECTOR_SDIV ] = RewriteSdiv; d_rewriteTable [ kind::BITVECTOR_SREM ] = RewriteSrem; diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index c50a3bbe0..59a2f90f6 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -39,7 +39,7 @@ class TheoryBVRewriter { static void initializeRewrites(); - static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false); + static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false); static RewriteResponse RewriteUlt(TNode node, bool prerewrite = false); static RewriteResponse RewriteSlt(TNode node, bool prerewrite = false); static RewriteResponse RewriteUle(TNode node, bool prerewrite = false); @@ -63,6 +63,8 @@ class TheoryBVRewriter { static RewriteResponse RewriteNeg(TNode node, bool prerewrite = false); static RewriteResponse RewriteUdiv(TNode node, bool prerewrite = false); static RewriteResponse RewriteUrem(TNode node, bool prerewrite = false); + static RewriteResponse RewriteUdivTotal(TNode node, bool prerewrite = false); + static RewriteResponse RewriteUremTotal(TNode node, bool prerewrite = false); static RewriteResponse RewriteSmod(TNode node, bool prerewrite = false); static RewriteResponse RewriteSdiv(TNode node, bool prerewrite = false); static RewriteResponse RewriteSrem(TNode node, bool prerewrite = false); diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am index 05c66d60c..7e5bcba8c 100644 --- a/test/regress/regress0/unconstrained/Makefile.am +++ b/test/regress/regress0/unconstrained/Makefile.am @@ -16,6 +16,8 @@ export CVC4_REGRESSION_ARGS # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" # dejan: disable arith2.smt2, arith7.smt2 it's mixed arithmetic and it doesn't go well when changing theoryof +# lianah: disabled bvdiv.smt2, bvconcat.smt2 as the unconstrained terms are no longer recognized after implementing +# the divide-by-zero semantics for bv division. TESTS = \ arith3.smt2 \ arith4.smt2 \ @@ -28,9 +30,7 @@ TESTS = \ bvbool.smt2 \ bvcmp.smt2 \ bvconcat2.smt2 \ - bvconcat.smt2 \ bvdiv2.smt2 \ - bvdiv.smt2 \ bvext.smt2 \ bvite.smt2 \ bvmul2.smt2 \ diff --git a/test/regress/regress0/unconstrained/bvdiv2.smt2 b/test/regress/regress0/unconstrained/bvdiv2.smt2 index 6314701b3..7a8fc3753 100644 --- a/test/regress/regress0/unconstrained/bvdiv2.smt2 +++ b/test/regress/regress0/unconstrained/bvdiv2.smt2 @@ -18,9 +18,9 @@ (declare-fun v4 () (_ BitVec 1024)) (declare-fun v5 () (_ BitVec 1024)) (assert - (not - (= (bvudiv x0 x0) (_ bv1 10)) - ) -) + (and + (not (= x0 (_ bv0 10))) + (not (= (bvudiv x0 x0) (_ bv1 10))) +)) (check-sat) (exit) -- 2.30.2