Restore tests directory

tests/bitv/testfile-array-cs.dolmen.smt2

@@ -0,0 +1,10 @@
+(set-logic ALL)
+; We need produce-models to propagate `int2bv` when learning `0 = y`
+(set-option :produce-models true)
+(declare-const a (Array Int Int))
+(declare-const x Int)
+(declare-const y Int)
+(assert (= (select a 4) 1))
+(assert (= (select (store a y 0) 4) 0))
+(assert (= ((_ int2bv 2) y) #b11))
+(check-sat)

tests/bitv/testfile-bv2nat-delayed.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/bitv/testfile-bv2nat-delayed.dolmen.smt2

@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-const x (_ BitVec 32))
+(assert (distinct (bv2nat x) 2))
+(assert (= x #b00000000000000000000000000000010))
+(check-sat)

tests/bitv/testfile-bv2nat-immediate.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/bitv/testfile-bv2nat-immediate.dolmen.smt2

@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-const x (_ BitVec 32))
+(assert (= x #b00000000000000000000000000000010))
+(assert (distinct (bv2nat x) 2))
+(check-sat)

tests/bitv/testfile-bv2nat-models.dolmen.expected

@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun x () (_ BitVec 4) #x7)
+)

tests/bitv/testfile-bv2nat-models.dolmen.smt2

@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const x (_ BitVec 4))
+(assert (= (bv2nat x) 7))
+(check-sat)
+(get-model)

tests/bitv/testfile-bvadd-001.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/bitv/testfile-bvadd-001.dolmen.smt2

@@ -0,0 +1,6 @@
+(set-logic ALL)
+(declare-const x (_ BitVec 1024))
+(declare-const y (_ BitVec 1024))
+; Addition of low bits is independent from high bits
+(assert (distinct ((_ extract 3 0) (bvadd (concat x #b0101) (concat y #b1100))) #b0001))
+(check-sat)

tests/bitv/testfile-bvadd-002.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/bitv/testfile-bvadd-002.dolmen.smt2

@@ -0,0 +1,8 @@
+(set-logic ALL)
+(declare-const x (_ BitVec 1024))
+(declare-const y (_ BitVec 1024))
+(declare-const z (_ BitVec 1024))
+(declare-const w (_ BitVec 1024))
+; Double zero stops carries
+(assert (distinct ((_ extract 1027 1025) (bvadd (concat x (concat #b0100 y)) (concat y (concat #b1100 z)))) #b000))
+(check-sat)

tests/bitv/testfile-bvand-001.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/bitv/testfile-bvand-001.dolmen.smt2

@@ -0,0 +1,4 @@
+(set-logic ALL)
+(declare-const x (_ BitVec 8))
+(assert (distinct #b00000000 (bvand x (bvnot x))))
+(check-sat)

tests/bitv/testfile-bvnot-term.dolmen.smt2

@@ -0,0 +1,7 @@
+(set-logic BV)
+
+(declare-const x (_ BitVec 4))
+(declare-const y (_ BitVec 4))
+(assert (= x (bvnot y)))
+(assert (distinct y x))
+(check-sat)

tests/bitv/testfile-bvor-001.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/bitv/testfile-bvor-001.dolmen.smt2

@@ -0,0 +1,4 @@
+(set-logic ALL)
+(declare-const x (_ BitVec 8))
+(assert (distinct #b11111111 (bvor x (bvnot x))))
+(check-sat)

tests/bitv/testfile-bvsub-001.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/bitv/testfile-bvsub-001.dolmen.smt2

@@ -0,0 +1,6 @@
+(set-logic ALL)
+(declare-const x (_ BitVec 1024))
+(declare-const y (_ BitVec 1024))
+; Subtraction of low bits is independent of high bits
+(assert (distinct ((_ extract 3 0) (bvsub (concat x #b0101) (concat y #b0111))) #b1110))
+(check-sat)

tests/bitv/testfile-bvsub-002.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/bitv/testfile-bvsub-002.dolmen.smt2

@@ -0,0 +1,8 @@
+(set-logic ALL)
+(declare-const x (_ BitVec 1024))
+(declare-const y (_ BitVec 1024))
+(declare-const z (_ BitVec 1024))
+(declare-const w (_ BitVec 1024))
+; Double zero stops carries
+(assert (distinct ((_ extract 1027 1025) (bvsub (concat x (concat #b0101 y)) (concat y (concat #b0100 z)))) #b000))
+(check-sat)

tests/bitv/testfile-bvxor-001.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/bitv/testfile-bvxor-001.dolmen.smt2

@@ -0,0 +1,4 @@
+(set-logic ALL)
+(declare-const x (_ BitVec 8))
+(assert (= x (bvxor #b10100101 x)))
+(check-sat)

tests/bitv/testfile-int2bv-delayed.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/bitv/testfile-int2bv-delayed.dolmen.smt2

@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-const x Int)
+(assert (distinct ((_ int2bv 4) x) #b0101))
+(assert (= x 5))
+(check-sat)

tests/bitv/testfile-int2bv-immediate.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/bitv/testfile-int2bv-immediate.dolmen.smt2

@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-const x Int)
+(assert (= x 5))
+(assert (distinct ((_ int2bv 4) x) #b0101))
+(check-sat)

tests/bitv/testfile-qfbv-timeout.unix.dolmen.expected

@@ -0,0 +1,9 @@
+
+unknown
+(:reason-unknown (:timeout :assume))
+
+unknown
+(:reason-unknown (:timeout :assume))
+
+unknown
+(:reason-unknown (:timeout :assume))

tests/bitv/testfile-qfbv-timeout.unix.dolmen.smt2

@@ -0,0 +1,58 @@
+(set-info :smt-lib-version 2.6)
+(set-option :reproducible-resource-limit 1)
+(set-logic QF_BV)
+(set-info :source |
+ Patrice Godefroid, SAGE (systematic dynamic test generation)
+ For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf
+|)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun T4_11167 () (_ BitVec 32))
+(declare-fun T2_10410 () (_ BitVec 16))
+(declare-fun T2_10408 () (_ BitVec 16))
+(declare-fun T2_10475 () (_ BitVec 16))
+(declare-fun T2_10473 () (_ BitVec 16))
+(declare-fun T2_10532 () (_ BitVec 16))
+(declare-fun T2_10530 () (_ BitVec 16))
+(declare-fun T2_10606 () (_ BitVec 16))
+(declare-fun T2_10604 () (_ BitVec 16))
+(declare-fun T2_10669 () (_ BitVec 16))
+(declare-fun T2_10667 () (_ BitVec 16))
+(declare-fun T2_10734 () (_ BitVec 16))
+(declare-fun T2_10736 () (_ BitVec 16))
+(declare-fun T1_11167 () (_ BitVec 8))
+(declare-fun T1_11168 () (_ BitVec 8))
+(declare-fun T1_11169 () (_ BitVec 8))
+(declare-fun T1_11170 () (_ BitVec 8))
+(declare-fun T1_10736 () (_ BitVec 8))
+(declare-fun T1_10737 () (_ BitVec 8))
+(declare-fun T1_10734 () (_ BitVec 8))
+(declare-fun T1_10735 () (_ BitVec 8))
+(declare-fun T1_10669 () (_ BitVec 8))
+(declare-fun T1_10670 () (_ BitVec 8))
+(declare-fun T1_10667 () (_ BitVec 8))
+(declare-fun T1_10668 () (_ BitVec 8))
+(declare-fun T1_10606 () (_ BitVec 8))
+(declare-fun T1_10607 () (_ BitVec 8))
+(declare-fun T1_10604 () (_ BitVec 8))
+(declare-fun T1_10605 () (_ BitVec 8))
+(declare-fun T1_10532 () (_ BitVec 8))
+(declare-fun T1_10533 () (_ BitVec 8))
+(declare-fun T1_10530 () (_ BitVec 8))
+(declare-fun T1_10531 () (_ BitVec 8))
+(declare-fun T1_10475 () (_ BitVec 8))
+(declare-fun T1_10476 () (_ BitVec 8))
+(declare-fun T1_10473 () (_ BitVec 8))
+(declare-fun T1_10474 () (_ BitVec 8))
+(declare-fun T1_10410 () (_ BitVec 8))
+(declare-fun T1_10411 () (_ BitVec 8))
+(declare-fun T1_10408 () (_ BitVec 8))
+(declare-fun T1_10409 () (_ BitVec 8))
+(assert (let ((?v_0 (bvadd T4_11167 (_ bv4 32))) (?v_12 ((_ zero_extend 16) T2_10408))) (let ((?v_10 (bvadd ?v_0 (bvsub (bvadd (bvadd (bvadd ?v_0 (_ bv61 32)) ?v_12) ((_ zero_extend 16) T2_10410)) ?v_0)))) (let ((?v_1 (bvadd ?v_10 (_ bv4 32))) (?v_18 ((_ zero_extend 16) T2_10473))) (let ((?v_16 (bvadd ?v_1 (bvsub (bvadd (bvadd (bvadd ?v_1 (_ bv53 32)) ?v_18) ((_ zero_extend 16) T2_10475)) ?v_1)))) (let ((?v_2 (bvadd ?v_16 (_ bv4 32))) (?v_24 ((_ zero_extend 16) T2_10530))) (let ((?v_22 (bvadd ?v_2 (bvsub (bvadd (bvadd (bvadd ?v_2 (_ bv70 32)) ?v_24) ((_ zero_extend 16) T2_10532)) ?v_2)))) (let ((?v_3 (bvadd ?v_22 (_ bv4 32))) (?v_30 ((_ zero_extend 16) T2_10604))) (let ((?v_28 (bvadd ?v_3 (bvsub (bvadd (bvadd (bvadd ?v_3 (_ bv59 32)) ?v_30) ((_ zero_extend 16) T2_10606)) ?v_3)))) (let ((?v_4 (bvadd ?v_28 (_ bv4 32))) (?v_36 ((_ zero_extend 16) T2_10667))) (let ((?v_34 (bvadd ?v_4 (bvsub (bvadd (bvadd (bvadd ?v_4 (_ bv63 32)) ?v_36) ((_ zero_extend 16) T2_10669)) ?v_4)))) (let ((?v_5 (bvadd ?v_34 (_ bv4 32)))) (let ((?v_40 (bvadd ?v_5 (_ bv42 32))) (?v_39 ((_ zero_extend 16) T2_10734)) (?v_38 (bvadd ?v_4 (_ bv42 32))) (?v_37 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_5) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_35 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_34) (_ bv0 32)) (_ bv1 8) (_ bv0 8)))))) (let ((?v_33 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_40) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_32 (bvadd ?v_3 (_ bv42 32))) (?v_31 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_4) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_29 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_28) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_27 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_38) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_26 (bvadd ?v_2 (_ bv42 32))) (?v_25 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_3) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_23 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_22) (_ bv0 32)) (_ bv1 8) (_ bv0 8)))))) (let ((?v_21 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_32) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_20 (bvadd ?v_1 (_ bv42 32))) (?v_19 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_2) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_17 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_16) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_15 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_26) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_14 (bvadd ?v_0 (_ bv42 32))) (?v_13 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_1) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_11 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_10) (_ bv0 32)) (_ bv1 8) (_ bv0 8)))))) (let ((?v_9 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_20) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_8 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_0) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_7 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) T4_11167) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_6 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_14) (_ bv0 32)) (_ bv1 8) (_ bv0 8)))))) (and true (= T2_10408 (bvor (bvshl ((_ zero_extend 8) T1_10409) (_ bv8 16)) ((_ zero_extend 8) T1_10408))) (= T2_10410 (bvor (bvshl ((_ zero_extend 8) T1_10411) (_ bv8 16)) ((_ zero_extend 8) T1_10410))) (= T2_10473 (bvor (bvshl ((_ zero_extend 8) T1_10474) (_ bv8 16)) ((_ zero_extend 8) T1_10473))) (= T2_10475 (bvor (bvshl ((_ zero_extend 8) T1_10476) (_ bv8 16)) ((_ zero_extend 8) T1_10475))) (= T2_10530 (bvor (bvshl ((_ zero_extend 8) T1_10531) (_ bv8 16)) ((_ zero_extend 8) T1_10530))) (= T2_10532 (bvor (bvshl ((_ zero_extend 8) T1_10533) (_ bv8 16)) ((_ zero_extend 8) T1_10532))) (= T2_10604 (bvor (bvshl ((_ zero_extend 8) T1_10605) (_ bv8 16)) ((_ zero_extend 8) T1_10604))) (= T2_10606 (bvor (bvshl ((_ zero_extend 8) T1_10607) (_ bv8 16)) ((_ zero_extend 8) T1_10606))) (= T2_10667 (bvor (bvshl ((_ zero_extend 8) T1_10668) (_ bv8 16)) ((_ zero_extend 8) T1_10667))) (= T2_10669 (bvor (bvshl ((_ zero_extend 8) T1_10670) (_ bv8 16)) ((_ zero_extend 8) T1_10669))) (= T2_10734 (bvor (bvshl ((_ zero_extend 8) T1_10735) (_ bv8 16)) ((_ zero_extend 8) T1_10734))) (= T2_10736 (bvor (bvshl ((_ zero_extend 8) T1_10737) (_ bv8 16)) ((_ zero_extend 8) T1_10736))) (= T4_11167 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_11170) (_ bv8 32)) ((_ zero_extend 24) T1_11169)) (_ bv8 32)) ((_ zero_extend 24) T1_11168)) (_ bv8 32)) ((_ zero_extend 24) T1_11167))) (bvslt (bvadd ?v_5 (bvsub (bvadd (bvadd (bvadd ?v_5 (_ bv64 32)) ?v_39) ((_ zero_extend 16) T2_10736)) ?v_5)) (_ bv0 32)) (bvult (_ bv0 32) ?v_6) (bvule (_ bv0 32) ?v_6) (bvult (_ bv0 32) ?v_7) (bvule (_ bv0 32) ?v_7) (bvult (_ bv0 32) ?v_8) (bvule (_ bv0 32) ?v_8) (bvult (_ bv0 32) ?v_9) (bvule (_ bv0 32) ?v_9) (bvult (_ bv0 32) ?v_11) (bvule (_ bv0 32) ?v_11) (= ?v_12 (_ bv0 32)) (bvult (_ bv0 32) ?v_13) (bvule (_ bv0 32) ?v_13) (not (= ?v_14 (_ bv4294967295 32))) (bvule (_ bv0 32) T4_11167) (not (= T4_11167 (_ bv11151 32))) (bvule T4_11167 (_ bv11151 32)) (not (= T4_11167 (_ bv4294967295 32))) (bvult (_ bv0 32) ?v_15) (bvule (_ bv0 32) ?v_15) (bvult (_ bv0 32) ?v_17) (bvule (_ bv0 32) ?v_17) (= ?v_18 (_ bv0 32)) (not (= ?v_0 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_0) (bvult (_ bv0 32) ?v_19) (bvule (_ bv0 32) ?v_19) (not (= ?v_20 (_ bv4294967295 32))) (not (= ?v_10 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_10) (bvult (_ bv0 32) ?v_21) (bvule (_ bv0 32) ?v_21) (bvult (_ bv0 32) ?v_23) (bvule (_ bv0 32) ?v_23) (= ?v_24 (_ bv0 32)) (not (= ?v_1 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_1) (bvult (_ bv0 32) ?v_25) (bvule (_ bv0 32) ?v_25) (not (= ?v_26 (_ bv4294967295 32))) (not (= ?v_16 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_16) (bvult (_ bv0 32) ?v_27) (bvule (_ bv0 32) ?v_27) (bvult (_ bv0 32) ?v_29) (bvule (_ bv0 32) ?v_29) (= ?v_30 (_ bv0 32)) (not (= ?v_2 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_2) (bvult (_ bv0 32) ?v_31) (bvule (_ bv0 32) ?v_31) (not (= ?v_32 (_ bv4294967295 32))) (not (= ?v_22 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_22) (bvult (_ bv0 32) ?v_33) (bvule (_ bv0 32) ?v_33) (bvult (_ bv0 32) ?v_35) (bvule (_ bv0 32) ?v_35) (= ?v_36 (_ bv0 32)) (not (= ?v_3 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_3) (bvult (_ bv0 32) ?v_37) (bvule (_ bv0 32) ?v_37) (not (= ?v_38 (_ bv4294967295 32))) (not (= ?v_28 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_28) (= ?v_39 (_ bv0 32)) (not (= ?v_4 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_4) (not (= ?v_40 (_ bv4294967295 32))) (not (= ?v_34 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_34) (not (= ?v_5 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_5))))))))))))))))))
+(check-sat)
+(get-info :reason-unknown)
+(check-sat)
+(get-info :reason-unknown)
+(check-sat)
+(get-info :reason-unknown)
+(exit)

tests/dolmen/bitv/bv2nat_bvneg.dolmen.smt2

@@ -0,0 +1,7 @@
+(set-logic ALL)
+
+; This is true, but we are not able to prove it for now due to lack of
+; algebraic reasoning on bit-vectors
+(declare-const x (_ BitVec 64))
+(assert (distinct (bv2nat (bvneg x)) (mod (+ (bv2nat (bvnot x)) 1) 18446744073709551616)))
+(check-sat)

tests/dolmen/bitv/bv2nat_bvnot.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/dolmen/bitv/bv2nat_bvnot.dolmen.smt2

@@ -0,0 +1,5 @@
+(set-logic ALL)
+
+(declare-const x (_ BitVec 64))
+(assert (distinct (bv2nat (bvnot x)) (- 18446744073709551615 (bv2nat x))))
+(check-sat)

tests/dolmen/bitv/bv2nat_bvnot_range.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/dolmen/bitv/bv2nat_bvnot_range.dolmen.smt2

@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-option :produce-models true)
+
+(declare-const x (_ BitVec 64))
+(assert (not (and (<= (bv2nat (bvnot x)) 18446744073709551615) (<= 0 (bv2nat (bvnot x))))))
+(check-sat)

tests/dolmen/bitv/coherence.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/dolmen/bitv/coherence.dolmen.smt2

@@ -0,0 +1,6 @@
+(set-logic ALL)
+(declare-const x (_ BitVec 2))
+(assert (= x (concat ((_ extract 0 0) x) ((_ extract 1 1) x))))
+(declare-fun f ((_ BitVec 2)) Int)
+(assert (distinct (f x) (f (concat ((_ extract 0 0) x) ((_ extract 1 1) x)))))
+(check-sat)

tests/dolmen/bitv/cyclic.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/dolmen/bitv/cyclic.dolmen.smt2

@@ -0,0 +1,7 @@
+(set-logic QF_BV)
+
+(declare-const x (_ BitVec 3))
+(assert (= ((_ extract 1 0) x) (bvnot ((_ extract 2 1) x))))
+(assert (= ((_ extract 0 0) x) #b0))
+(assert (distinct x #b010))
+(check-sat)

tests/dolmen/bitv/not-contra.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/dolmen/bitv/not-contra.dolmen.smt2

@@ -0,0 +1,7 @@
+(set-logic BV)
+(set-option :produce-models true)
+
+(declare-const x (_ BitVec 2))
+(assert (= (bvnot x) #b00))
+(assert (= x #b00))
+(check-sat)

tests/dolmen/bitv/notextract.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/dolmen/bitv/notextract.dolmen.smt2

@@ -0,0 +1,8 @@
+(set-logic QF_BV)
+
+(declare-const x (_ BitVec 64))
+(declare-const y (_ BitVec 64))
+
+(assert (= ((_ extract 32 16) x) (bvnot ((_ extract 32 16) y))))
+(assert (= ((_ extract 32 0) x) ((_ extract 32 0) y)))
+(check-sat)

tests/dolmen/bitv/notnotx.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/dolmen/bitv/notnotx.dolmen.smt2

@@ -0,0 +1,5 @@
+(set-logic QF_BV)
+
+(declare-const x (_ BitVec 64))
+(assert (distinct (bvnot (bvnot x)) x))
+(check-sat)

tests/dolmen/bitv/notx.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/dolmen/bitv/notx.dolmen.smt2

@@ -0,0 +1,5 @@
+(set-logic QF_BV)
+
+(declare-const x (_ BitVec 64))
+(assert (= (bvnot x) x))
+(check-sat)

tests/float/test_float1.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/float/test_float1.dolmen.smt2

@@ -0,0 +1,6 @@
+(set-logic ALL)
+
+(declare-const x Real)
+(assert (> x 0.0))
+(assert (= ((_ ae.round 1 1) RTZ 0.3) x))
+(check-sat)

tests/float/test_float2.models.expected

@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun x () Real (/ 1 4))
+)

tests/float/test_float2.models.smt2

@@ -0,0 +1,8 @@
+(set-logic ALL)
+
+(set-option :produce-models true)
+(declare-const x Real)
+(assert (> x 0.0))
+(assert (= ((_ ae.round 1 2) RTZ 0.3) x))
+(check-sat)
+(get-model)

tests/issues/555.models.expected

@@ -0,0 +1,8 @@
+
+unknown
+(
+  (define-fun x () Int 0)
+  (define-fun y () Int 0)
+  (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
+  (define-fun a2 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0))
+)

tests/issues/555.models.smt2

@@ -0,0 +1,12 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const x Int)
+(declare-const y Int)
+(declare-const a1 (Array Int Int))
+(declare-const a2 (Array Int Int))
+(assert (= (select a1 x) x))
+(assert (= (store a1 x y) a1))
+(assert (= (select a2 x) x))
+(assert (= (store a2 x y) a1))
+(check-sat)
+(get-model)

tests/issues/649/649.dolmen.smt2

@@ -0,0 +1,10 @@
+(set-logic BV)
+(declare-const x (_ BitVec 2))
+(assert (
+    exists
+      ((y (_ BitVec 4)))
+      (distinct
+        (concat (concat ((_ extract 3 3) y) ((_ extract 3 3) y)) y)
+        (concat (concat (_ bv0 2) x) (_ bv0 2))
+)))
+(check-sat)

tests/issues/664/664.dolmen.expected

@@ -0,0 +1,2 @@
+
+unknown

tests/issues/664/664.dolmen.smt2

@@ -0,0 +1,7 @@
+(set-logic QF_BV)
+(declare-fun T () (_ BitVec 2))
+(assert
+  (and
+    (distinct T (_ bv0 2))
+    (= (_ bv0 2) (concat (_ bv0 1) ((_ extract 0 0) T)))))
+(check-sat)

tests/issues/777.models.expected

@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun i () Int 1)
+)

tests/issues/777.models.smt2

@@ -0,0 +1,7 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const i Int)
+(define-fun C ((j Int)) Bool (> j 0))
+(assert (C i))
+(check-sat)
+(get-model)

tests/issues/854/function.models.expected

@@ -0,0 +1,8 @@
+
+unknown
+(
+  (define-fun a () Int 0)
+  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref))
+  (define-fun f ((_arg_0 Int)) Int 0)
+  (define-fun a1 () Int 0)
+)