arith-interval.cvc « integers « arith « 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/arith/integers/arith-interval.cvc

blob: ed6cb747e6a0c4cd05fd6d785783c76460b6004c (plain)

% EXPECT: entailed
x: INT;
P: INT -> BOOLEAN;

ASSERT 1 <= x AND x <= 2;
ASSERT P(1) AND P(2);
QUERY P(x);

generated by cgit on debian on lair

contact matthew@masot.net with questions or feedback