issue4275-qcf-cegqi-rep.smt2 « quantifiers « 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/quantifiers/issue4275-qcf-cegqi-rep.smt2

blob: 6caa2b10cbc96dad94626db37e2a604493e907fc (plain)

(set-logic UFBV)
(set-option :cegqi-all true)
(set-info :status unsat)
(declare-sort S0 0)
(declare-const S0-0 S0)
(declare-const v6 Bool)
(assert (forall ((q0 (_ BitVec 10)) (q1 S0) (q2 S0) (q3 Bool)) (xor true (and q3 q3 q3 v6 q3 q3) (= q2 q1 S0-0))))
(check-sat)

generated by cgit on debian on lair

contact matthew@masot.net with questions or feedback