Wed, 17 Nov 2010 09:22:23 +0100 require the b2i file ending in the boogie_open command (for consistency with the theory header)
boehmes [Wed, 17 Nov 2010 09:22:23 +0100] rev 40580
require the b2i file ending in the boogie_open command (for consistency with the theory header)
Wed, 17 Nov 2010 08:14:56 +0100 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes [Wed, 17 Nov 2010 08:14:56 +0100] rev 40579
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
Wed, 17 Nov 2010 08:14:55 +0100 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes [Wed, 17 Nov 2010 08:14:55 +0100] rev 40578
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip