issue3687-check-models-small.smt2 « aufbv « regress0 « regress « test - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

index : cvc5.git

CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

git repository hosting

summary refs log tree commit diff

path: root/test/regress/regress0/aufbv/issue3687-check-models-small.smt2

blob: 88cbd8a0ba2d31ebe58727328af7606535ad62a1 (plain)

; COMMAND-LINE: --check-models
; EXPECT: sat
(set-logic QF_AUFBV)
(declare-fun a () (Array (_ BitVec 2) (_ BitVec 2)))
(declare-fun b () (_ BitVec 2))
(assert (distinct #b01 (select (store (store a #b01 (bvor #b01 (select a
  #b00))) #b10 #b00) b)))
(check-sat)

generated by cgit on debian on lair

contact matthew@masot.net with questions or feedback