Fr_neg.ini

rdi := nondet as dst          
rsi := nondet as src1          
      
assume dst & 0b111 = 0         
assume src1 & 0b111 = 0          
      
assume 0x1000 <= dst <= 0x2000  
assume src1 = 0x4000  ## arbitrary range  

#assume @[src1, 8] = 0x8000000000000000
#assume @[src1+8, 32] = 0x0000000000000000000000000000000000000000000000000000000000000002
#assume @[src1+8, 32] = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
#assume @[src1, 40] = 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f00000008000000000000000
starting from <Fr_neg> with
    assume 0x7ffff000000 <= rsp <= 0x7ffff800000 # arbitrary stack range
    @[rsp, 8] := <Fr_neg:last>   # set the return address
end

replace <Fr_neg:last> by
  
  eq<1> := true
  if @[src1 + 4, 32] = 0 then #short
    if @[src1, 8] = 0x0000000080000000 then #overflow
      eq := eq && @[dst, 40] =  0x00000000000000000000000000000000000000000000000000000000800000008000000000000000
    else # General
      eq := eq && @[dst, 4] = -@[src1, 4]
    end
  end   
      print @[src1, 40]
      print @[dst, 40]
      print @[dst + 8, 32] + @[src1 + 8, 32] 
  if @[src1, 8] = 0x8000000000000000 then # long
    # 0
    if @[src1, 40] = 0x00000000000000000000000000000000000000000000000000000000000000008000000000000000 then
      eq := eq && @[src1, 40] = @[dst, 40]
    else # general
      eq := eq && @[dst + 8, 32] + @[src1 + 8, 32] = 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
    end
  end
  assert eq  
  halt
end
#0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
explore all