search

favu100 / b2program

READ-ONLY MIRROR of https://gitlab.cs.uni-duesseldorf.de/general/stups/b2program; DO NOT PUSH
5 stars 3 forks source link

Fix symbol not found error in ExplicitChecks.mch #17

Closed leuschel closed 1 month ago

leuschel commented 2 years ago

when commenting in

( #(f,y).((f = %x.(x : 0..100|x + y) & y=1000 & f(5) = 1005)) )

we get this error

make ExplicitChecks LANGUAGE=java DIRECTORY=benchmarks/model_checking/ProB/Other java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/Other/ExplicitChecks.mch cp benchmarks/model_checking/ProB/Other/*.java . javac -cp .:btypes.jar ExplicitChecks.java ExplicitChecks.java:156: error: cannot find symbol _ic_set_7 = _ic_set_7.union(new BRelation<BInteger, BInteger>(new BTuple<>(_ic_x_1, _ic_x_1.plus(y)))); ^ symbol: variable y location: class ExplicitChecks 1 error

favu100 commented 2 years ago

This should not be possible as the bounded variables are enumerated in the order they are defined. This should be detected by the code generator

favu100 commented 1 month ago

This predicate is now allowed by B2Program and the issue is fixed now