Potential Unsoundness in Prelude.bpl #4400
Description
I naively took Prelude.bpl and added this to the end (otherwise boogie would not emit an SMT file).
procedure should_not_prove()
ensures false;
{
}
I then ran boogie (version 3.0.0) to log the generated SMT query (dotnet version 6.0.412):
dotnet tool run boogie DafnyPrelude.bpl /proverLog:DafnyPrelude.smt2
I ran this with vampire (version 4.8), it reported that a refutation (unsat):
% Refutation found. Thanks to Tanya!
% SZS status Unsatisfiable for DafnyPrelude
% SZS output start Proof for DafnyPrelude
113. ! [X1 : 'T@Box()',X0 : 'Array'('T@Box()',$int)] : $sum($select(X0,X1),1) = $select('MultiSet#UnionOne_12626'(X0,X1),X1) [input]
122. ! [X2 : 'T@Box()',X1 : 'T@Box()',X0 : 'Array'('T@Box()',$int)] : ($less(0,$select('MultiSet#UnionOne_12626'(X0,X1),X2)) <=> (X1 = X2 | $less(0,$select(X0,X2)))) [input]
412. $sum(X0,X1) = $sum(X1,X0) [theory axiom 138]
416. 0 = $sum(X0,$uminus(X0)) [theory axiom 143]
445. $select($store(X3,X0,X2),X0) = X2 [theory axiom 177]
590. ! [X0 : 'T@Box()',X1 : 'T@Box()',X2 : 'Array'('T@Box()',$int)] : ($less(0,$select('MultiSet#UnionOne_12626'(X2,X1),X0)) <=> (X0 = X1 | $less(0,$select(X2,X0)))) [rectify 122]
595. ! [X0 : 'T@Box()',X1 : 'Array'('T@Box()',$int)] : $sum($select(X1,X0),1) = $select('MultiSet#UnionOne_12626'(X1,X0),X0) [rectify 113]
995. ! [X0 : 'T@Box()',X1 : 'T@Box()',X2 : 'Array'('T@Box()',$int)] : (($less(0,$select('MultiSet#UnionOne_12626'(X2,X1),X0)) | (X0 != X1 & ~$less(0,$select(X2,X0)))) & ((X0 = X1 | $less(0,$select(X2,X0))) | ~$less(0,$select('MultiSet#UnionOne_12626'(X2,X1),X0)))) [nnf transformation 590]
996. ! [X0 : 'T@Box()',X1 : 'T@Box()',X2 : 'Array'('T@Box()',$int)] : (($less(0,$select('MultiSet#UnionOne_12626'(X2,X1),X0)) | (X0 != X1 & ~$less(0,$select(X2,X0)))) & (X0 = X1 | $less(0,$select(X2,X0)) | ~$less(0,$select('MultiSet#UnionOne_12626'(X2,X1),X0)))) [flattening 995]
1410. $less(0,$select('MultiSet#UnionOne_12626'(X2,X1),X0)) | X0 != X1 [cnf transformation 996]
1420. $sum($select(X1,X0),1) = $select('MultiSet#UnionOne_12626'(X1,X0),X0) [cnf transformation 595]
1743. $less(0,$select('MultiSet#UnionOne_12626'(X2,X1),X1)) [equality resolution 1410]
1811. $select('MultiSet#UnionOne_12626'(X1,X0),X0) = $sum(1,$select(X1,X0)) [forward demodulation 1420,412]
1812. $less(0,$sum(1,$select(X2,X1))) [backward demodulation 1743,1811]
2253. $less(0,$sum(1,X5)) [superposition 1812,445]
2258. $less(0,0) [superposition 2253,416]
2261. $false [evaluation 2258]
From the proof, it seems like these two axioms from Prelude.bpl are causing the problem:
// pure containment axiom (in the original multiset or is the added element)
axiom (forall<T> a: MultiSet T, x: T, o: T :: { MultiSet#UnionOne(a,x)[o] }
0 < MultiSet#UnionOne(a,x)[o] <==> o == x || 0 < a[o]);
// union-ing increases count by one
axiom (forall<T> a: MultiSet T, x: T :: { MultiSet#UnionOne(a, x) }
MultiSet#UnionOne(a, x)[x] == a[x] + 1);
I removed the two conflicting asserts from the SMT file, a new refutation was found. In fact there seemed to be 4 disjoint sets of conflicting asserts. That is, I repeated the following until vampire was not able to immediately find a refutation, and 4 disjoint sets of asserts were reported:
- remove all conflicting asserts in one refutation
vampirefinds a new refutation