tests

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

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))))

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)

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))))

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)

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)
+