issue4225-univ-fun.smt2 « fmf « 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/fmf/issue4225-univ-fun.smt2

blob: 9946a4567a2895425e994be1dd666fa5e84405ff (plain)

; COMMAND-LINE: --finite-model-find --uf-ho
; EXPECT: unknown
(set-logic ALL)
; this is not handled by fmf
(assert (forall ((a (-> Int Int)) (b Int)) (not (= (a b) 0))))
(check-sat)

generated by cgit on debian on lair

contact matthew@masot.net with questions or feedback