From 59e839cc8266e75f96883a5a047e1672938afb54 Mon Sep 17 00:00:00 2001 From: Yoni Zohar Date: Fri, 6 Oct 2023 00:46:35 +0300 Subject: [PATCH] tests --- test/regress/cli/CMakeLists.txt | 3 + .../cli/regress0/bv/bv_to_int_9071.smt2 | 4 +- .../cli/regress0/bv/bv_to_int_9071_bv4.smt2 | 6 ++ .../regress0/bv/bv_to_int_9071_th_sym.smt2 | 4 +- .../cli/regress1/bv/bv_to_int_10084.smt2 | 16 +++++ .../regress1/bv/bv_to_int_10084_forall.smt2 | 72 +++++++++++++++++++ 6 files changed, 99 insertions(+), 6 deletions(-) create mode 100644 test/regress/cli/regress0/bv/bv_to_int_9071_bv4.smt2 create mode 100644 test/regress/cli/regress1/bv/bv_to_int_10084.smt2 create mode 100644 test/regress/cli/regress1/bv/bv_to_int_10084_forall.smt2 diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 7110a6bd76c..52d5108237d 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -295,6 +295,7 @@ set(regress_0_tests regress0/bv/bv_to_int_5293_2.smt2 regress0/bv/bv_to_int_8412.smt2 regress0/bv/bv_to_int_9071.smt2 + regress0/bv/bv_to_int_9071_bv4.smt2 regress0/bv/bv_to_int_9071_th_sym.smt2 regress0/bv/bv_to_int_bvmul2.smt2 regress0/bv/bv_to_int_bvuf_to_intuf.smt2 @@ -2065,6 +2066,8 @@ set(regress_1_tests regress1/bv/bench_38.delta.smt2 regress1/bv/bug787.smt2 regress1/bv/bug_extract_mult_leading_bit.smt2 + regress1/bv/bv_to_int_10084.smt2 + regress1/bv/bv_to_int_10084_forall.smt2 regress1/bv/bv-int-collapse2-sat.smt2 regress1/bv/bv-proof00.smtv1.smt2 regress1/bv/bv2nat-ground.smt2 diff --git a/test/regress/cli/regress0/bv/bv_to_int_9071.smt2 b/test/regress/cli/regress0/bv/bv_to_int_9071.smt2 index 25406d28f5e..5e5bc61d548 100644 --- a/test/regress/cli/regress0/bv/bv_to_int_9071.smt2 +++ b/test/regress/cli/regress0/bv/bv_to_int_9071.smt2 @@ -1,7 +1,5 @@ -; EXPECT: -; SCRUBBER: grep -v "quantified.variables" +; EXPECT: sat ; COMMAND-LINE: --solve-bv-as-int=iand -; EXIT: 1 (set-logic UFBV) (declare-fun x ((_ BitVec 1)) (_ BitVec 1)) (assert (exists ((y (_ BitVec 1))) (= (x y) (_ bv0 1)))) diff --git a/test/regress/cli/regress0/bv/bv_to_int_9071_bv4.smt2 b/test/regress/cli/regress0/bv/bv_to_int_9071_bv4.smt2 new file mode 100644 index 00000000000..ccfb06d61cf --- /dev/null +++ b/test/regress/cli/regress0/bv/bv_to_int_9071_bv4.smt2 @@ -0,0 +1,6 @@ +; EXPECT: sat +; COMMAND-LINE: --solve-bv-as-int=iand +(set-logic UFBV) +(declare-fun x ((_ BitVec 4)) (_ BitVec 4)) +(assert (exists ((y (_ BitVec 4))) (= (x y) (_ bv0 4)))) +(check-sat) diff --git a/test/regress/cli/regress0/bv/bv_to_int_9071_th_sym.smt2 b/test/regress/cli/regress0/bv/bv_to_int_9071_th_sym.smt2 index d0b2f05e80d..8780bdf7ab7 100644 --- a/test/regress/cli/regress0/bv/bv_to_int_9071_th_sym.smt2 +++ b/test/regress/cli/regress0/bv/bv_to_int_9071_th_sym.smt2 @@ -1,7 +1,5 @@ -; EXPECT: -; SCRUBBER: grep -v "quantified.variables" +; EXPECT: sat ; COMMAND-LINE: --solve-bv-as-int=iand -; EXIT: 1 (set-logic UFBV) (declare-fun x ((_ BitVec 1)) (_ BitVec 1)) (assert (exists ((y (_ BitVec 1))) (= (x (bvnot y)) (_ bv0 1)))) diff --git a/test/regress/cli/regress1/bv/bv_to_int_10084.smt2 b/test/regress/cli/regress1/bv/bv_to_int_10084.smt2 new file mode 100644 index 00000000000..98567b556c8 --- /dev/null +++ b/test/regress/cli/regress1/bv/bv_to_int_10084.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --solve-bv-as-int=iand +; EXPECT: unsat + +(set-logic ALL) + +(declare-const x (_ BitVec 16)) +(declare-const y (_ BitVec 16)) +(declare-const z (_ BitVec 16)) + +(assert + (not + (=> + (bvule x y) + (bvule (bvmul ((_ zero_extend 48) x) ((_ zero_extend 48) z)) (bvmul ((_ zero_extend 48) y) ((_ zero_extend 48) z)))))) + +(check-sat) diff --git a/test/regress/cli/regress1/bv/bv_to_int_10084_forall.smt2 b/test/regress/cli/regress1/bv/bv_to_int_10084_forall.smt2 new file mode 100644 index 00000000000..38db99e557d --- /dev/null +++ b/test/regress/cli/regress1/bv/bv_to_int_10084_forall.smt2 @@ -0,0 +1,72 @@ +; COMMAND-LINE: --solve-bv-as-int=iand +; EXPECT: unsat + +;; produced by cvc4_16.drv ;; +(set-logic AUFBVFPDTNIRA) +;; produced by cvc4_16.drv +(set-info :smt-lib-version 2.6) +;;; generated by SMT-LIB2 driver +;;; SMT-LIB2 driver: bit-vectors, common part +;;; SMT-LIB2: integer arithmetic +(declare-datatypes ((tuple0 0)) + (((Tuple0)))) + +(declare-sort us_private 0) + +(declare-const us_null_ext__ us_private) + +;; "in_range" +(define-fun in_range ((x Int)) Bool + (and (<= (- 2147483648) x) (<= x 2147483647))) + +;; "value" +(declare-fun value (tuple0) Int) + +;; "value__function_guard" +(declare-fun value__function_guard (Int + tuple0) Bool) + +;; "value__post_axiom" +(assert + (forall ((us_void_param tuple0)) + (! (let ((result (value us_void_param))) + (=> (value__function_guard result us_void_param) (in_range result))) :pattern ( + (value + us_void_param)) ))) + +;; "f1" +(declare-fun f1 (tuple0) Int) + +;; "f1__function_guard" +(declare-fun f1__function_guard (Int + tuple0) Bool) + +;; "f1__post_axiom" +(assert + (forall ((us_void_param tuple0)) + (! (let ((result (f1 us_void_param))) + (=> (f1__function_guard result us_void_param) (in_range result))) :pattern ( + (f1 + us_void_param)) ))) + +;; "f1__def_axiom" +(assert + (forall ((us_void_param tuple0)) + (! (= (f1 us_void_param) 1) :pattern ((f1 us_void_param)) ))) + +;; Goal "def'vc" +;; File "main.adb", line 4, characters 0-0 +(assert + (not + (let ((temp___210 (value Tuple0))) + (=> + (and (value__function_guard temp___210 Tuple0) (in_range temp___210)) + (forall ((spark__branch Bool)) + (=> + (= spark__branch (ite (= temp___210 0) true false)) + (=> + (= spark__branch true) + (=> (f1__function_guard (f1 Tuple0) Tuple0) (= (f1 Tuple0) 1))))))))) + +(check-sat) +