nl_uf_lalt.smt2 « nl « regress1 « 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/regress1/nl/nl_uf_lalt.smt2

blob: c5ccd322f68ad5a5b234ca00397252c030679aad (plain)

; COMMAND-LINE: --no-check-unsat-cores
(set-logic QF_UFNIA)
(set-info :status unsat)
(declare-fun c (Int) Int)
(declare-fun a (Int) Int)
(declare-fun b (Int) Int)
(assert (> (a 0) 0))
(assert (= (c 0) (* (a 0) (b 0))))
(assert (not (= (b 0) (div (c 0) (a 0)))))
(check-sat)

generated by cgit on debian on lair

contact matthew@masot.net with questions or feedback