run_small.jsscript from github and modifying it while building the image. I wanted to ask you if it was okay to include this file (via download or just the plain file) in the image repo
smtsolver.availableSolversto eldarica (or whichever solver you want) + modified settings
>>Intis translated to
shrIntin smt, but I can't find a definition of
maxUInt48 &Int (X >>Int 48)means "give me the second lowest 48 bits"
rule maxUInt48 &Int (X >>Int 48) => projectSecondLowest48(X)
project...functions which can be used.