Special-case unary minus in a different way

Author: geo2a

kore/src/Kore/Rewrite/SMT/Translate.hs

@@ -533,6 +533,11 @@ backTranslateWith
         backTranslate (List xs)
             | null xs =
                 throwError "backtranslate: empty list"
+            -- special case for the unary minus, back-translating 'List ["-", "X"]' as '0 - X'
+            | [fct@(Atom "-"), arg] <- xs
+            , Just koreSym <- Map.lookup fct reverseMetadata = do
+                arg' <- backTranslate arg
+                pure $ TermLike.mkApplySymbol koreSym [mkInternalInt (InternalInt (simpleSort "SortInt") 0), arg']
             -- everything is translated back using symbol declarations,
             -- not ML connectives (translating terms not predicates)
             | (fct@Atom{} : rest) <- xs