diff options
23 files changed, 134 insertions, 34 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 4e1a89259..683fe61bd 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -642,6 +642,12 @@ header = "options/smt_options.h" [[option.mode.SUM]] name = "sum" help = "Generate a sum expression for each bvand instance, based on the value in --solbv-bv-as-int-granularity" +[[option.mode.IAND]] + name = "iand" + help = "Translate bvand to the iand operator (experimental)" +[[option.mode.BV]] + name = "bv" + help = "Translate bvand back to bit-vectors" [[option]] name = "BVAndIntegerGranularity" diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index aa1b5ac5b..9ee4e2b7d 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -169,7 +169,8 @@ Node BVToInt::eliminationPass(Node n) { current = toVisit.back(); // assert that the node is binarized - kind::Kind_t k = current.getKind(); + // The following variable is only used in assertions + CVC4_UNUSED kind::Kind_t k = current.getKind(); uint64_t numChildren = current.getNumChildren(); Assert((numChildren == 2) || !(k == kind::BITVECTOR_PLUS || k == kind::BITVECTOR_MULT @@ -350,7 +351,8 @@ Node BVToInt::translateWithChildren(Node original, // ultbv and sltbv were supposed to be eliminated before this point. Assert(oldKind != kind::BITVECTOR_ULTBV); Assert(oldKind != kind::BITVECTOR_SLTBV); - uint64_t originalNumChildren = original.getNumChildren(); + // The following variable will only be used in assertions. + CVC4_UNUSED uint64_t originalNumChildren = original.getNumChildren(); Node returnNode; switch (oldKind) { @@ -414,15 +416,43 @@ Node BVToInt::translateWithChildren(Node original, } case kind::BITVECTOR_AND: { - // Construct an ite, based on granularity. + // We support three configurations: + // 1. translating to IAND + // 2. translating back to BV (using BITVECTOR_TO_NAT and INT_TO_BV + // operators) + // 3. translating into a sum uint64_t bvsize = original[0].getType().getBitVectorSize(); - Assert(translated_children.size() == 2); - Node newNode = createBitwiseNode(translated_children[0], + if (options::solveBVAsInt() == options::SolveBVAsIntMode::IAND) + { + Node iAndOp = d_nm->mkConst(IntAnd(bvsize)); + returnNode = d_nm->mkNode( + kind::IAND, iAndOp, translated_children[0], translated_children[1]); + } + else if (options::solveBVAsInt() == options::SolveBVAsIntMode::BV) + { + // translate the children back to BV + Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize)); + Node x = translated_children[0]; + Node y = translated_children[1]; + Node bvx = d_nm->mkNode(intToBVOp, x); + Node bvy = d_nm->mkNode(intToBVOp, y); + // perform bvand on the bit-vectors + Node bvand = d_nm->mkNode(kind::BITVECTOR_AND, bvx, bvy); + // translate the result to integers + returnNode = d_nm->mkNode(kind::BITVECTOR_TO_NAT, bvand); + } + else + { + Assert(options::solveBVAsInt() == options::SolveBVAsIntMode::SUM); + // Construct a sum of ites, based on granularity. + Assert(translated_children.size() == 2); + Node newNode = createBitwiseNode(translated_children[0], translated_children[1], bvsize, options::BVAndIntegerGranularity(), &oneBitAnd); - returnNode = newNode; + returnNode = newNode; + } break; } case kind::BITVECTOR_SHL: diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 87b3c7310..bc45a3105 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -220,12 +220,8 @@ set(regress_0_tests regress0/bv/bv-to-bool1.smtv1.smt2 regress0/bv/bv-to-bool2.smt2 regress0/bv/bv_to_int1.smt2 - regress0/bv/bv_to_int2.smt2 - regress0/bv/bv_to_int_bvmul1.smt2 regress0/bv/bv_to_int_bvmul2.smt2 - regress0/bv/bv_to_int_bitwise.smt2 regress0/bv/bv_to_int_bvuf_to_intuf.smt2 - regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 regress0/bv/bv_to_int_elim_err.smt2 regress0/bv/bv_to_int_zext.smt2 @@ -2102,7 +2098,11 @@ set(regress_2_tests regress2/bug765.smt2 regress2/bug812.smt2 regress2/bv/opStructure_MBA_6.scrambled.min.smt2 + regress2/bv_to_int2.smt2 regress2/bv_to_int_ashr.smt2 + regress2/bv_to_int_bitwise.smt2 + regress2/bv_to_int_bvmul1.smt2 + regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 regress2/bv_to_int_inc1.smt2 regress2/bv_to_int_mask_array_1.smt2 regress2/bv_to_int_mask_array_2.smt2 @@ -2201,8 +2201,12 @@ set(regress_3_tests regress3/bmc-ibm-5.smtv1.smt2 regress3/bmc-ibm-7.smtv1.smt2 regress3/bv_to_int_and_or.smt2 + regress3/bv_to_int_bench_9839.smt2.minimized.smt2 regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2 + regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2 + regress3/bv_to_int_quant1.smt2 + regress3/bv_to_int_quant2.smt2 regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2 regress3/eq_diamond14.smtv1.smt2 regress3/friedman_n6_i4.smtv1.smt2 diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2 index 970a9fd75..9111ac25c 100644 --- a/test/regress/regress0/bv/bv_to_int1.smt2 +++ b/test/regress/regress0/bv/bv_to_int1.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun x () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 index 4bbe5685e..91e0c45fd 100644 --- a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun T4_180 () (_ BitVec 32)) diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 index 5879542eb..3e545ef03 100644 --- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 ; EXPECT: sat (set-logic QF_UFBV) (declare-fun a () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 index f43c8c860..0a0ec7b20 100644 --- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 ; EXPECT: sat (set-logic QF_UFBV) (declare-sort S 0) diff --git a/test/regress/regress0/bv/bv_to_int2.smt2 b/test/regress/regress2/bv_to_int2.smt2 index d60f4903b..4c1ca0c00 100644 --- a/test/regress/regress0/bv/bv_to_int2.smt2 +++ b/test/regress/regress2/bv_to_int2.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 ; EXPECT: sat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2 index 11952839f..5516f974b 100644 --- a/test/regress/regress2/bv_to_int_ashr.smt2 +++ b/test/regress/regress2/bv_to_int_ashr.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress0/bv/bv_to_int_bitwise.smt2 b/test/regress/regress2/bv_to_int_bitwise.smt2 index 444551776..373f9c323 100644 --- a/test/regress/regress0/bv/bv_to_int_bitwise.smt2 +++ b/test/regress/regress2/bv_to_int_bitwise.smt2 @@ -1,5 +1,7 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=iand --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_BV) (declare-fun s () (_ BitVec 4)) diff --git a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 b/test/regress/regress2/bv_to_int_bvmul1.smt2 index e21415244..cfd5c4b9a 100644 --- a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 +++ b/test/regress/regress2/bv_to_int_bvmul1.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-unsat-cores -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 ; EXPECT: sat (set-logic QF_BV) (declare-fun a () (_ BitVec 8)) diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 index 6196b2bb9..babf9af32 100644 --- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 +++ b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 @@ -1,6 +1,5 @@ -;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-models --no-produce-unsat-cores +;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-unsat-cores ;EXPECT: unsat - (set-logic QF_UFBV) (declare-fun z$n0s32 () (_ BitVec 32)) (declare-fun dataOut () (_ BitVec 32)) diff --git a/test/regress/regress2/bv_to_int_inc1.smt2 b/test/regress/regress2/bv_to_int_inc1.smt2 index 0d09a7252..4b22c8ed8 100644 --- a/test/regress/regress2/bv_to_int_inc1.smt2 +++ b/test/regress/regress2/bv_to_int_inc1.smt2 @@ -1,4 +1,6 @@ ; COMMAND-LINE: --incremental --solve-bv-as-int=sum +; COMMAND-LINE: --incremental --solve-bv-as-int=iand +; COMMAND-LINE: --incremental --solve-bv-as-int=bv ; EXPECT sat ; EXPECT sat ; EXPECT unsat diff --git a/test/regress/regress2/bv_to_int_mask_array_1.smt2 b/test/regress/regress2/bv_to_int_mask_array_1.smt2 index 970f27fb9..b1c8b9509 100644 --- a/test/regress/regress2/bv_to_int_mask_array_1.smt2 +++ b/test/regress/regress2/bv_to_int_mask_array_1.smt2 @@ -1,4 +1,6 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=iand --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores ; EXPECT: unsat (set-logic ALL) (declare-fun A () (Array Int Int)) diff --git a/test/regress/regress2/bv_to_int_mask_array_2.smt2 b/test/regress/regress2/bv_to_int_mask_array_2.smt2 index 0960b9359..c054f9693 100644 --- a/test/regress/regress2/bv_to_int_mask_array_2.smt2 +++ b/test/regress/regress2/bv_to_int_mask_array_2.smt2 @@ -1,4 +1,6 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 +; COMMAND-LINE: --solve-bv-as-int=iand +; COMMAND-LINE: --solve-bv-as-int=bv ; EXPECT: sat (set-logic ALL) (declare-fun A () (Array Int Int)) diff --git a/test/regress/regress2/bv_to_int_mask_array_3.smt2 b/test/regress/regress2/bv_to_int_mask_array_3.smt2 index 329ee715a..37582d9d8 100644 --- a/test/regress/regress2/bv_to_int_mask_array_3.smt2 +++ b/test/regress/regress2/bv_to_int_mask_array_3.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores +; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores ; EXPECT: sat (set-logic ALL) (declare-fun A () (Array (_ BitVec 4) (_ BitVec 4))) diff --git a/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2 new file mode 100644 index 000000000..aeacda35e --- /dev/null +++ b/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --solve-bv-as-int=bv +; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=sum +; EXPECT: sat +(set-logic QF_BV) +(declare-fun _substvar_1171_ () (_ BitVec 32)) +(assert (bvsge ((_ sign_extend 0) _substvar_1171_) (_ bv0 32))) +(check-sat) +(exit) diff --git a/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2 index a2c964e9a..67f8f69ad 100644 --- a/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2 +++ b/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=sum --no-check-models -; COMMAND-LINE: --cegqi-all --full-saturate-quant --bvand-integer-granularity=2 --solve-bv-as-int=sum --no-check-models +; COMMAND-LINE: --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=sum --no-check-models +; COMMAND-LINE: --cegqi-all --full-saturate-quant --bvand-integer-granularity=2 --solve-bv-as-int=sum --no-check-models ; EXPECT: sat (set-logic BV) (declare-fun s () (_ BitVec 3)) diff --git a/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 new file mode 100644 index 000000000..300883882 --- /dev/null +++ b/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --solve-bv-as-int=bv +; COMMAND-LINE: --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=sum +; COMMAND-LINE: --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=iand --iand-mode=sum +; COMMAND-LINE: --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=iand --iand-mode=bitwise +; COMMAND-LINE: --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=iand +; COMMAND-LINE: --cegqi-all --full-saturate-quant --bvand-integer-granularity=2 --solve-bv-as-int=sum +; EXPECT: unsat +(set-logic ALL) +(declare-fun t () (_ BitVec 4)) +(declare-fun s () (_ BitVec 4)) +(assert (bvult (_ bv8 4) (bvadd (_ bv8 4) (bvlshr t s)))) +(assert (forall ((x (_ BitVec 4))) (bvule (bvadd (_ bv8 4) (bvlshr x s)) (_ bv8 4)))) +(check-sat) +(exit) diff --git a/test/regress/regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2 index 22656d17f..1db79b1e9 100644 --- a/test/regress/regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2 +++ b/test/regress/regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores ; COMMAND-LINE: --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=sum --no-check-unsat-cores ; EXPECT: unsat (set-logic BV) diff --git a/test/regress/regress3/bv_to_int_quant1.smt2 b/test/regress/regress3/bv_to_int_quant1.smt2 new file mode 100644 index 000000000..22656d17f --- /dev/null +++ b/test/regress/regress3/bv_to_int_quant1.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=sum --no-check-unsat-cores +; EXPECT: unsat +(set-logic BV) +(declare-fun s () (_ BitVec 4)) +(assert (bvult s (_ bv4 4))) +(assert (forall ((x (_ BitVec 4))) (= (bvlshr x s) (_ bv0 4)))) +(check-sat) +(exit) diff --git a/test/regress/regress3/bv_to_int_quant2.smt2 b/test/regress/regress3/bv_to_int_quant2.smt2 new file mode 100644 index 000000000..c2bf6d9d0 --- /dev/null +++ b/test/regress/regress3/bv_to_int_quant2.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cegqi-all --full-saturate-quant --solve-bv-as-int=sum --no-check-models +; COMMAND-LINE: --cegqi-all --full-saturate-quant --solve-bv-as-int=bv --no-check-models +; COMMAND-LINE: --cegqi-all --full-saturate-quant --solve-bv-as-int=iand --no-check-models +; EXPECT: sat +(set-logic BV) +(declare-fun s () (_ BitVec 4)) +(assert (bvult s (_ bv4 4))) +(assert (forall ((x (_ BitVec 4))) (= (bvand x s) (_ bv0 4)))) +(check-sat) +(exit) diff --git a/test/regress/regress3/bv_to_int_signed_sub_or.smt2 b/test/regress/regress3/bv_to_int_signed_sub_or.smt2 new file mode 100644 index 000000000..50cce4511 --- /dev/null +++ b/test/regress/regress3/bv_to_int_signed_sub_or.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores +; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=sum --no-check-unsat-cores +; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=iand --iand-mode=value --no-check-unsat-cores +; COMMAND-LINE: --bvand-integer-granularity=2 --solve-bv-as-int=sum --no-check-unsat-cores +; EXPECT: unsat +(set-logic QF_BV) +(declare-fun s () (_ BitVec 4)) +(declare-fun t () (_ BitVec 4)) +(assert (bvsgt s t)) +(assert (bvsge t (bvsub t (bvor (bvor s t) (bvneg s))))) +(check-sat) +(exit) |