-
Notifications
You must be signed in to change notification settings - Fork 13
Open
Labels
Description
It would be useful if we could test if some lemma works to discharge some node in the command line, without having to write the lemma in the lemmas file, rekompile and then run the proof again. Take the example where some node has the following constraint:
#And { maxUInt8 <Int bool2Word ( maxUInt128 <Int VV0_x_114b9705:Int ) <<Int 7 #Equals true }
And we want to easily check that the following lemma works to prove that the node has a contradiction:
rule A <Int bool2Word ( _ ) <<Int B => false
requires A >=Int 1 <<Int B
Instead of having to add the lemma to the lemmas file and then rekompile, it would be useful to be able to:
kontrol simplify-node testName nodeId "A <Int bool2Word ( _ ) <<Int B => false requires A >=Int 1 <<Int B"