bug168.smt « 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/bug168.smt

blob: 8fb0ddf5d2ddf71b86277076a5bd498384ce403b (plain)

(benchmark fuzzsmt
:logic QF_LRA
:extrafuns ((v0 Real))
:status sat
:formula
(let (?n1 3)
(flet ($n2 (distinct ?n1 v0))
$n2
)))

generated by cgit on debian on lair

contact matthew@masot.net with questions or feedback